1 /-
2 Copyright (c) 2018 Mario Carneiro. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Mario Carneiro
5 -/
6
7 import tactic.ring data.num.lemmas data.tree
src └─────────┘ └─────────────┘ └───────┘
8 import tactic.converter.interactive
src └──────────────────────────┘
9
10 /-!
11 # ring2
12
13 An experimental variant on the `ring` tactic that uses computational
14 reflection instead of proof generation. Useful for kernel benchmarking.
15 -/
16
17 namespace tree
18
19 /-- `(reflect' t u α)` quasiquotes a tree `(t: tree expr)` of quoted
20 values of type `α` at level `u` into an `expr` which reifies to a `tree α`
21 containing the reifications of the `expr`s from the original `t`. -/
22 protected meta def reflect' (u : level) (α : expr) : tree expr → expr
id └───┘ └──┘ └──┘ └──┘ ┴ └──┘
src └───┘ └──┘ └──┘ └──┘ └──┘
typ └───┘ └──┘ └──┘ └──┘ ┴ └──┘
doc └───┘ └──┘ └──┘ └──┘
23 | tree.nil := (expr.const ``tree.nil [u] : expr) α
id └──────┘ └────────┘ ┴ ┴┴┴ └──┘ ┴
src └──────┘ └────────┘ ┴ ┴ ┴ └──┘
typ └──────┘ └────────┘ ┴ ┴┴┴ └──┘ ┴
doc └──┘
24 | (tree.node a t₁ t₂) :=
id └───────┘ ┴ └┘ └┘
src └───────┘
typ └───────┘ ┴ └┘ └┘
25 (expr.const ``tree.node [u] : expr) α a t₁.reflect' t₂.reflect'
id └────────┘ ┴ ┴┴┴ └──┘ ┴
src └────────┘ ┴ ┴ ┴ └──┘
typ └────────┘ ┴ ┴┴┴ └──┘ ┴
doc └──┘
26
27 /-- Returns an element indexed by `n`, or zero if `n` isn't a valid index.
28 See `tree.get`. -/
29 protected def get_or_zero {α} [has_zero α] (t : tree α) (n : pos_num) : α :=
id └──────┘ ┴ └──┘ ┴ └─────┘ ┴
src └──────┘ └──┘ └─────┘
typ └──────┘ ┴ └──┘ ┴ └─────┘ ┴
doc └─────┘
30 t.get_or_else n 0
id ┴└──────────┘ ┴
src └──────────┘
typ ┴└──────────┘ ┴
doc └──────────┘
31
32 end tree
33
34 namespace tactic.ring2
35
36 /-- A reflected/meta representation of an expression in a commutative
37 semiring. This representation is a direct translation of such
38 expressions - see `horner_expr` for a normal form. -/
39 @[derive has_reflect]
id └─────────┘
src └─────────┘
typ └─────────┘
doc └────┘
40 inductive csring_expr
41 /- (atom n) is an opaque element of the csring. For example,
42 a local variable in the context. n indexes into a storage
43 of such atoms - a `tree α`. -/
44 | atom : pos_num → csring_expr
id └─────┘
src └─────┘
typ └─────┘
doc └─────┘
45 /- (const n) is technically the csring's one, added n times.
46 Or the zero if n is 0. -/
47 | const : num → csring_expr
id └─┘
src └─┘
typ └─┘
doc └─┘
48 | add : csring_expr → csring_expr → csring_expr
49 | mul : csring_expr → csring_expr → csring_expr
50 | pow : csring_expr → num → csring_expr
id └─┘
src └─┘
typ └─┘
doc └─┘
51
52 namespace csring_expr
53
54 instance : inhabited csring_expr := ⟨const 0⟩
id └───────┘ └─────────┘ └───┘
src └───────┘ └─────────┘ └───┘
typ └───────┘ └─────────┘ └───┘
doc └─────────┘
55
56 /-- Evaluates a reflected `csring_expr` into an element of the
57 original `comm_semiring` type `α`, retrieving opaque elements
58 (atoms) from the tree `t`. -/
59 def eval {α} [comm_semiring α] (t : tree α) : csring_expr → α
id └───────────┘ ┴ └──┘ ┴ └─────────┘ ┴ ┴
src └───────────┘ └──┘ └─────────┘
typ └───────────┘ ┴ └──┘ ┴ └─────────┘ ┴ ┴
doc └─────────┘
60 | (atom n) := t.get_or_zero n
id └──┘ ┴ ┴└──────────┘
src └──┘ └──────────┘
typ └──┘ ┴ ┴└──────────┘
doc └──────────┘
61 | (const n) := n
id └───┘ ┴
src └───┘
typ └───┘ ┴
62 | (add x y) := eval x + eval y
id └─┘ ┴ ┴ └──┘ ┴ └──┘
src └─┘ ┴
typ └─┘ ┴ ┴ └──┘ ┴ └──┘
63 | (mul x y) := eval x * eval y
id └─┘ ┴ ┴ └──┘ ┴ └──┘
src └─┘ ┴
typ └─┘ ┴ ┴ └──┘ ┴ └──┘
64 | (pow x n) := eval x ^ (n : ℕ)
id └─┘ ┴ ┴ └──┘ ┴ ┴
src └─┘ ┴ ┴
typ └─┘ ┴ ┴ └──┘ ┴ ┴
65
66 end csring_expr
67
68 /-- An efficient representation of expressions in a commutative
69 semiring using the sparse Horner normal form. This type admits
70 non-optimal instantiations (e.g. `P` can be represented as `P+0+0`),
71 so to get good performance out of it, care must be taken to maintain
72 an optimal, *canonical* form. -/
73 @[derive decidable_eq]
id └──────────┘
src └──────────┘
typ └──────────┘
doc └────┘
74 inductive horner_expr
75 /- (const n) is a constant n in the csring, similarly to the same
76 constructor in `csring_expr`. This one, however, can be negative. -/
77 | const : znum → horner_expr
id └──┘
src └──┘
typ └──┘
doc └──┘
78 /- (horner a x n b) is a*xⁿ + b, where x is the x-th atom
79 in the atom tree. -/
80 | horner : horner_expr → pos_num → num → horner_expr → horner_expr
id └─────┘ └─┘
src └─────┘ └─┘
typ └─────┘ └─┘
doc └─────┘ └─┘
81
82 namespace horner_expr
83
84 /-- True iff the `horner_expr` argument is a valid `csring_expr`.
85 For that to be the case, all its constants must be non-negative. -/
86 def is_cs : horner_expr → Prop
id └─────────┘ ┴
src └─────────┘
typ └─────────┘ ┴
doc └─────────┘
87 | (const n) := ∃ m:num, n = m.to_znum
id └───┘ ┴ ┴ └─┘┴ ┴ ┴└──────┘
src └───┘ ┴ └─┘┴ ┴ └──────┘
typ └───┘ ┴ ┴ └─┘┴ ┴ ┴└──────┘
doc └─┘
88 | (horner a x n b) := is_cs a ∧ is_cs b
id └────┘ ┴ ┴ └───┘ ┴ └───┘
src └────┘ ┴
typ └────┘ ┴ ┴ └───┘ ┴ └───┘
89
90 instance : has_zero horner_expr := ⟨const 0⟩
id └──────┘ └─────────┘ └───┘
src └──────┘ └─────────┘ └───┘
typ └──────┘ └─────────┘ └───┘
doc └─────────┘
91 instance : has_one horner_expr := ⟨const 1⟩
id └─────┘ └─────────┘ └───┘
src └─────┘ └─────────┘ └───┘
typ └─────┘ └─────────┘ └───┘
doc └─────────┘
92 instance : inhabited horner_expr := ⟨0⟩
id └───────┘ └─────────┘
src └───────┘ └─────────┘
typ └───────┘ └─────────┘
doc └─────────┘
93
94 /-- Represent a `csring_expr.atom` in Horner form. -/
95 def atom (n : pos_num) : horner_expr := horner 1 n 1 0
id └─────┘ └─────────┘ └────┘ ┴
src └─────┘ └─────────┘ └────┘
typ └─────┘ └─────────┘ └────┘ ┴
doc └─────┘ └─────────┘
96
97 def to_string : horner_expr → string
id └─────────┘ ┴ └────┘
src └─────────┘ ┴ └────┘
typ └─────────┘ ┴ └────┘
doc └─────────┘
98 | (const n) := _root_.repr n
id └───┘ ┴ └─────────┘
src └───┘ └─────────┘
typ └───┘ ┴ └─────────┘
99 | (horner a x n b) :=
id └────┘ ┴ ┴ ┴ ┴
src └────┘
typ └────┘ ┴ ┴ ┴ ┴
100 "(" ++ to_string a ++ ") * x" ++ _root_.repr x ++ "^"
id └┘ └───────┘ └┘ └┘ └─────────┘ └┘
src └┘ └───────┘ └┘ └┘ └─────────┘ └┘
typ └┘ └───────┘ └┘ └┘ └─────────┘ └┘
101 ++ _root_.repr n ++ " + " ++ to_string b
id └┘ └─────────┘ └┘ └┘ └───────┘
src └┘ └─────────┘ └┘ └┘ └───────┘
typ └┘ └─────────┘ └┘ └┘ └───────┘
102 instance : has_to_string horner_expr := ⟨to_string⟩
id └───────────┘ └─────────┘ └───────┘
src └───────────┘ └─────────┘ └───────┘
typ └───────────┘ └─────────┘ └───────┘
doc └─────────┘
103
104 /-- Alternative constructor for (horner a x n b) which maintains canonical
105 form by simplifying special cases of `a`. -/
106 def horner' (a : horner_expr)
id └─────────┘
src └─────────┘
typ └─────────┘
doc └─────────┘
107 (x : pos_num) (n : num) (b : horner_expr) : horner_expr :=
id └─────┘ └─┘ └─────────┘ └─────────┘
src └─────┘ └─┘ └─────────┘ └─────────┘
typ └─────┘ └─┘ └─────────┘ └─────────┘
doc └─────┘ └─┘ └─────────┘ └─────────┘
108 match a with
id ┴
typ ┴
109 | const q := if q = 0 then b else horner a x n b
id └───┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
src └───┘ ┴ └────┘
typ └───┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
110 | horner a₁ x₁ n₁ b₁ :=
id └────┘ └┘ └┘ └┘ └┘
src └────┘
typ └────┘ └┘ └┘ └┘ └┘
111 if x₁ = x ∧ b₁ = 0 then horner a₁ x (n₁ + n) b
id ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └────┘ ┴
typ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
112 else horner a x n b
id └────┘ ┴ ┴ ┴ ┴
src └────┘
typ └────┘ ┴ ┴ ┴ ┴
113 end
114
115 def add_const (k : znum) (e : horner_expr) : horner_expr :=
id └──┘ └─────────┘ └─────────┘
src └──┘ └─────────┘ └─────────┘
typ └──┘ └─────────┘ └─────────┘
doc └──┘ └─────────┘ └─────────┘
116 if k = 0 then e else begin
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
st └─────
117 induction e with n a x n b A B,
id ┴
src └────────┘ └─────────────────┘
typ └────────┘┴└─────────────────┘
doc └────────┘ └─────────────────┘
txt └────────┘ └─────────────────┘
par └────────┘ └─────────────────┘
pid ┴ ┴└────────────────┘
st ───────────────────────────────┘└─
118 { exact const (k + n) },
id └───┘ ┴ ┴ ┴
src └────┘└───┘┴ ┴┴┴ └┘
typ └────┘└───┘┴ ┴┴┴┴┴└┘
doc └────┘ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴┴
st ───┘└──────────────────┘└┘└
119 { exact horner a x n B }
id └────┘ ┴ ┴ ┴ ┴
src └────┘└────┘┴ ┴ ┴ ┴ ┴
typ └────┘└────┘┴┴┴┴┴┴┴┴┴
doc └────┘ ┴ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────┘└─
120 end
st ──┘
121
122 def add_aux (a₁ : horner_expr) (A₁ : horner_expr → horner_expr) (x₁ : pos_num) :
id └─────────┘ └─────────┘ └─────────┘ └─────┘
src └─────────┘ └─────────┘ └─────────┘ └─────┘
typ └─────────┘ └─────────┘ └─────────┘ └─────┘
doc └─────────┘ └─────────┘ └─────────┘ └─────┘
123 horner_expr → num → horner_expr → (horner_expr → horner_expr) → horner_expr
id └─────────┘ ┴ └─┘ └─────────┘ └─────────┘ ┴ └─────────┘ └─────────┘
src └─────────┘ └─┘ └─────────┘ └─────────┘ └─────────┘ └─────────┘
typ └─────────┘ ┴ └─┘ └─────────┘ └─────────┘ ┴ └─────────┘ └─────────┘
doc └─────────┘ └─┘ └─────────┘ └─────────┘ └─────────┘ └─────────┘
124 | (const n₂) n₁ b₁ B₁ := add_const n₂ (horner a₁ x₁ n₁ b₁)
id └───┘ └┘ └┘ └┘ └───────┘ └────┘ └┘ └┘
src └───┘ └───────┘ └────┘
typ └───┘ └┘ └┘ └┘ └───────┘ └────┘ └┘ └┘
125 | (horner a₂ x₂ n₂ b₂) n₁ b₁ B₁ :=
id └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
src └────┘
typ └────┘ └┘ └┘ └┘ └┘ └┘ └┘ └┘
126 let e₂ := horner a₂ x₂ n₂ b₂ in
id └┘ └────┘
src └────┘
typ └┘ └────┘
127 match pos_num.cmp x₁ x₂ with
id └─────────┘ └┘
src └─────────┘
typ └─────────┘ └┘
128 | ordering.lt := horner a₁ x₁ n₁ (B₁ e₂)
id └─────────┘ └────┘ └┘ └┘ └┘
src └─────────┘ └────┘
typ └─────────┘ └────┘ └┘ └┘ └┘
129 | ordering.gt := horner a₂ x₂ n₂ (add_aux b₂ n₁ b₁ B₁)
id └─────────┘ └────┘ └─────┘
src └─────────┘ └────┘
typ └─────────┘ └────┘ └─────┘
130 | ordering.eq :=
id └─────────┘
src └─────────┘
typ └─────────┘
131 match num.sub' n₁ n₂ with
id └──────┘
src └──────┘
typ └──────┘
132 | znum.zero := horner' (A₁ a₂) x₁ n₁ (B₁ b₂)
id └───────┘ └─────┘ └┘ └┘
src └───────┘ └─────┘
typ └───────┘ └─────┘ └┘ └┘
doc └─────┘
133 | (znum.pos k) := horner (add_aux a₂ k 0 id) x₁ n₂ (B₁ b₂)
id └──────┘ ┴ └────┘ └─────┘ └┘ └┘
src └──────┘ └────┘ └┘
typ └──────┘ ┴ └────┘ └─────┘ └┘ └┘
134 | (znum.neg k) := horner (A₁ (horner a₂ x₁ k 0)) x₁ n₁ (B₁ b₂)
id └──────┘ ┴ └────┘ └┘ └────┘ └┘ └┘
src └──────┘ └────┘ └────┘
typ └──────┘ ┴ └────┘ └┘ └────┘ └┘ └┘
135 end
136 end
137
138 def add : horner_expr → horner_expr → horner_expr
id └─────────┘ ┴ └─────────┘ └─────────┘
src └─────────┘ └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ └─────────┘
doc └─────────┘ └─────────┘ └─────────┘
139 | (const n₁) e₂ := add_const n₁ e₂
id └───┘ └┘ └┘ └───────┘
src └───┘ └───────┘
typ └───┘ └┘ └┘ └───────┘
140 | (horner a₁ x₁ n₁ b₁) e₂ := add_aux a₁ (add a₁) x₁ e₂ n₁ b₁ (add b₁)
id └────┘ └┘ └┘ └┘ └┘ └┘ └─────┘ └─┘ └─┘
src └────┘ └─────┘
typ └────┘ └┘ └┘ └┘ └┘ └┘ └─────┘ └─┘ └─┘
141 /-begin
142 induction e₁ with n₁ a₁ x₁ n₁ b₁ A₁ B₁ generalizing e₂,
143 { exact add_const n₁ e₂ },
144 exact match e₂ with e₂ := begin
145 induction e₂ with n₂ a₂ x₂ n₂ b₂ A₂ B₂ generalizing n₁ b₁;
146 let e₁ := horner a₁ x₁ n₁ b₁,
147 { exact add_const n₂ e₁ },
148 let e₂ := horner a₂ x₂ n₂ b₂,
149 exact match pos_num.cmp x₁ x₂ with
150 | ordering.lt := horner a₁ x₁ n₁ (B₁ e₂)
151 | ordering.gt := horner a₂ x₂ n₂ (B₂ n₁ b₁)
152 | ordering.eq :=
153 match num.sub' n₁ n₂ with
154 | znum.zero := horner' (A₁ a₂) x₁ n₁ (B₁ b₂)
155 | (znum.pos k) := horner (A₂ k 0) x₁ n₂ (B₁ b₂)
156 | (znum.neg k) := horner (A₁ (horner a₂ x₁ k 0)) x₁ n₁ (B₁ b₂)
157 end
158 end
159 end end
160 end-/
161
162 def neg (e : horner_expr) : horner_expr :=
id └─────────┘ └─────────┘
src └─────────┘ └─────────┘
typ └─────────┘ └─────────┘
doc └─────────┘ └─────────┘
163 begin
st └─────
164 induction e with n a x n b A B,
id ┴
src └────────┘ └─────────────────┘
typ └────────┘┴└─────────────────┘
doc └────────┘ └─────────────────┘
txt └────────┘ └─────────────────┘
par └────────┘ └─────────────────┘
pid ┴ ┴└────────────────┘
st ───────────────────────────────┘└─
165 { exact const (-n) },
id └───┘ ┴┴
src └────┘└───┘┴ ┴ └┘
typ └────┘└───┘┴ ┴┴└┘
doc └────┘ ┴ └┘
txt └────┘ ┴ └┘
par └────┘ ┴ └┘
pid ┴ ┴ ┴┴
st ───┘└───────────────┘└┘└
166 { exact horner A x n B }
id └────┘ ┴ ┴ ┴ ┴
src └────┘└────┘┴ ┴ ┴ ┴ ┴
typ └────┘└────┘┴┴┴┴┴┴┴┴┴
doc └────┘ ┴ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────┘└─
167 end
st ──┘
168
169 def mul_const (k : znum) (e : horner_expr) : horner_expr :=
id └──┘ └─────────┘ └─────────┘
src └──┘ └─────────┘ └─────────┘
typ └──┘ └─────────┘ └─────────┘
doc └──┘ └─────────┘ └─────────┘
170 if k = 0 then 0 else if k = 1 then e else begin
id ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴
st └─────
171 induction e with n a x n b A B,
id ┴
src └────────┘ └─────────────────┘
typ └────────┘┴└─────────────────┘
doc └────────┘ └─────────────────┘
txt └────────┘ └─────────────────┘
par └────────┘ └─────────────────┘
pid ┴ ┴└────────────────┘
st ───────────────────────────────┘└─
172 { exact const (n * k) },
id └───┘ ┴ ┴ ┴
src └────┘└───┘┴ ┴┴┴ └┘
typ └────┘└───┘┴ ┴┴┴┴┴└┘
doc └────┘ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴┴
st ───┘└──────────────────┘└┘└
173 { exact horner A x n B }
id └────┘ ┴ ┴ ┴ ┴
src └────┘└────┘┴ ┴ ┴ ┴ ┴
typ └────┘└────┘┴┴┴┴┴┴┴┴┴
doc └────┘ ┴ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────┘└─
174 end
st ──┘
175
176 def mul_aux (a₁ x₁ n₁ b₁) (A₁ B₁ : horner_expr → horner_expr) :
id └─────────┘ └─────────┘
src └─────────┘ └─────────┘
typ └─────────┘ └─────────┘
doc └─────────┘ └─────────┘
177 horner_expr → horner_expr
id └─────────┘ ┴ └─────────┘
src └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘
doc └─────────┘ └─────────┘
178 | (const n₂) := mul_const n₂ (horner a₁ x₁ n₁ b₁)
id └───┘ └┘ └───────┘ └────┘ └┘ └┘ └┘ └┘
src └───┘ └───────┘ └────┘
typ └───┘ └┘ └───────┘ └────┘ └┘ └┘ └┘ └┘
179 | e₂@(horner a₂ x₂ n₂ b₂) :=
id └────┘ └┘ └┘ └┘ └┘
src └────┘
typ └────┘ └┘ └┘ └┘ └┘
180 match pos_num.cmp x₁ x₂ with
id └─────────┘ └┘
src └─────────┘
typ └─────────┘ └┘
181 | ordering.lt := horner (A₁ e₂) x₁ n₁ (B₁ e₂)
id └─────────┘ └────┘ └┘ └┘ └┘ └┘
src └─────────┘ └────┘
typ └─────────┘ └────┘ └┘ └┘ └┘ └┘
182 | ordering.gt := horner (mul_aux a₂) x₂ n₂ (mul_aux b₂)
id └─────────┘ └────┘ └─────┘ └─────┘
src └─────────┘ └────┘
typ └─────────┘ └────┘ └─────┘ └─────┘
183 | ordering.eq := let haa := horner' (mul_aux a₂) x₁ n₂ 0 in
id └─────────┘ └─┘ └─────┘ └─────┘ └┘
src └─────────┘ └─────┘
typ └─────────┘ └─┘ └─────┘ └─────┘ └┘
doc └─────┘
184 if b₂ = 0 then haa else haa.add (horner (A₁ b₂) x₁ n₁ (B₁ b₂))
id ┴ └─┘ └─┘└──┘ └────┘ └┘ └┘ └┘ └┘
src ┴ └──┘ └────┘
typ ┴ └─┘ └─┘└──┘ └────┘ └┘ └┘ └┘ └┘
185 end
186
187 def mul : horner_expr → horner_expr → horner_expr
id └─────────┘ ┴ └─────────┘ └─────────┘
src └─────────┘ └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘ └─────────┘
doc └─────────┘ └─────────┘ └─────────┘
188 | (const n₁) := mul_const n₁
id └───┘ └┘ └───────┘
src └───┘ └───────┘
typ └───┘ └┘ └───────┘
189 | (horner a₁ x₁ n₁ b₁) := mul_aux a₁ x₁ n₁ b₁ (mul a₁) (mul b₁).
id └────┘ └┘ └┘ └┘ └┘ └─────┘ └─┘ └─┘
src └────┘ └─────┘
typ └────┘ └┘ └┘ └┘ └┘ └─────┘ └─┘ └─┘
190 /-begin
191 induction e₁ with n₁ a₁ x₁ n₁ b₁ A₁ B₁ generalizing e₂,
192 { exact mul_const n₁ e₂ },
193 induction e₂ with n₂ a₂ x₂ n₂ b₂ A₂ B₂;
194 let e₁ := horner a₁ x₁ n₁ b₁,
195 { exact mul_const n₂ e₁ },
196 let e₂ := horner a₂ x₂ n₂ b₂,
197 cases pos_num.cmp x₁ x₂,
198 { exact horner (A₁ e₂) x₁ n₁ (B₁ e₂) },
199 { let haa := horner' A₂ x₁ n₂ 0,
200 exact if b₂ = 0 then haa else
201 haa.add (horner (A₁ b₂) x₁ n₁ (B₁ b₂)) },
202 { exact horner A₂ x₂ n₂ B₂ }
203 end-/
204
205 instance : has_add horner_expr := ⟨add⟩
id └─────┘ └─────────┘ └─┘
src └─────┘ └─────────┘ └─┘
typ └─────┘ └─────────┘ └─┘
doc └─────────┘
206 instance : has_neg horner_expr := ⟨neg⟩
id └─────┘ └─────────┘ └─┘
src └─────┘ └─────────┘ └─┘
typ └─────┘ └─────────┘ └─┘
doc └─────────┘
207 instance : has_mul horner_expr := ⟨mul⟩
id └─────┘ └─────────┘ └─┘
src └─────┘ └─────────┘ └─┘
typ └─────┘ └─────────┘ └─┘
doc └─────────┘
208
209 def pow (e : horner_expr) : num → horner_expr
id └─────────┘ └─┘ ┴ └─────────┘
src └─────────┘ └─┘ └─────────┘
typ └─────────┘ └─┘ ┴ └─────────┘
doc └─────────┘ └─┘ └─────────┘
210 | 0 := 1
211 | (num.pos p) := begin
id └─────┘
src └─────┘
typ └─────┘
st └─────
212 induction p with p ep p ep,
id ┴
src └────────┘ └─────────────┘
typ └────────┘┴└─────────────┘
doc └────────┘ └─────────────┘
txt └────────┘ └─────────────┘
par └────────┘ └─────────────┘
pid ┴ ┴└────────────┘
st ───────────────────────────┘└─
213 { exact e },
id ┴
src └────┘ ┴
typ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└──────┘└┘└
214 { exact (ep.mul ep).mul e },
id └────┘ └┘ ┴
src └────┘ └────┘┴ └────┘ ┴
typ └────┘ └────┘┴└┘└────┘┴┴
doc └────┘ ┴ └────┘ ┴
txt └────┘ ┴ └────┘ ┴
par └────┘ ┴ └────┘ ┴
pid ┴ ┴ └────┘ ┴
st ───┘└──────────────────────┘└┘└
215 { exact ep.mul ep }
id └────┘ └┘
src └────┘└────┘┴ ┴
typ └────┘└────┘┴└┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ───────────────────┘└─
216 end
st ──┘
217
218 def inv (e : horner_expr) : horner_expr := 0
id └─────────┘ └─────────┘
src └─────────┘ └─────────┘
typ └─────────┘ └─────────┘
doc └─────────┘ └─────────┘
219
220 /-- Brings expressions into Horner normal form. -/
221 def of_csexpr : csring_expr → horner_expr
id └─────────┘ ┴ └─────────┘
src └─────────┘ └─────────┘
typ └─────────┘ ┴ └─────────┘
doc └─────────┘ └─────────┘
222 | (csring_expr.atom n) := atom n
id └──────────────┘ ┴ └──┘
src └──────────────┘ └──┘
typ └──────────────┘ ┴ └──┘
doc └──┘
223 | (csring_expr.const n) := const n.to_znum
id └───────────────┘ ┴ └───┘ └──────┘
src └───────────────┘ └───┘ └──────┘
typ └───────────────┘ ┴ └───┘ └──────┘
224 | (csring_expr.add x y) := (of_csexpr x).add (of_csexpr y)
id └─────────────┘ ┴ ┴ └───────┘ └─┘ └───────┘
src └─────────────┘ └─┘
typ └─────────────┘ ┴ ┴ └───────┘ └─┘ └───────┘
225 | (csring_expr.mul x y) := (of_csexpr x).mul (of_csexpr y)
id └─────────────┘ ┴ ┴ └───────┘ └─┘ └───────┘
src └─────────────┘ └─┘
typ └─────────────┘ ┴ ┴ └───────┘ └─┘ └───────┘
226 | (csring_expr.pow x n) := (of_csexpr x).pow n
id └─────────────┘ ┴ ┴ └───────┘ └─┘
src └─────────────┘ └─┘
typ └─────────────┘ ┴ ┴ └───────┘ └─┘
227
228 /-- Evaluates a reflected `horner_expr` - see `csring_expr.eval`. -/
229 def cseval {α} [comm_semiring α] (t : tree α) : horner_expr → α
id └───────────┘ ┴ └──┘ ┴ └─────────┘ ┴ ┴
src └───────────┘ └──┘ └─────────┘
typ └───────────┘ ┴ └──┘ ┴ └─────────┘ ┴ ┴
doc └─────────┘
230 | (const n) := n.abs
id └───┘ ┴ └──┘
src └───┘ └──┘
typ └───┘ ┴ └──┘
231 | (horner a x n b) := tactic.ring.horner (cseval a) (t.get_or_zero x) n (cseval b)
id └────┘ ┴ ┴ ┴ ┴ └────────────────┘ └────┘ ┴└──────────┘ └────┘
src └────┘ └────────────────┘ └──────────┘
typ └────┘ ┴ ┴ ┴ ┴ └────────────────┘ └────┘ ┴└──────────┘ └────┘
doc └──────────┘
232
233 theorem cseval_atom {α} [comm_semiring α] (t : tree α)
id └───────────┘ ┴ └──┘ ┴
src └───────────┘ └──┘
typ └───────────┘ ┴ └──┘ ┴
234 (n : pos_num) : (atom n).is_cs ∧ cseval t (atom n) = t.get_or_zero n :=
id └─────┘ └──┘ ┴ └───┘ ┴ └────┘ ┴ └──┘ ┴ ┴ ┴└──────────┘ ┴
src └─────┘ └──┘ └───┘ ┴ └────┘ └──┘ ┴ └──────────┘
typ └─────┘ └──┘ ┴ └───┘ ┴ └────┘ ┴ └──┘ ┴ ┴ ┴└──────────┘ ┴
doc └─────┘ └──┘ └───┘ └────┘ └──┘ └──────────┘
235 ⟨⟨⟨1, rfl⟩, ⟨0, rfl⟩⟩, (tactic.ring.horner_atom _).symm⟩
id └─┘ └─┘ └─────────────────────┘ └──┘
src └─┘ └─┘ └─────────────────────┘ └──┘
typ └─┘ └─┘ └─────────────────────┘ └──┘
236
237 theorem cseval_add_const {α} [comm_semiring α] (t : tree α)
id └───────────┘ ┴ └──┘ ┴
src └───────────┘ └──┘
typ └───────────┘ ┴ └──┘ ┴
238 (k : num) {e : horner_expr} (cs : e.is_cs) :
id └─┘ └─────────┘ ┴└────┘
src └─┘ └─────────┘ └────┘
typ └─┘ └─────────┘ ┴└────┘
doc └─┘ └─────────┘ └────┘
239 (add_const k.to_znum e).is_cs ∧
id └───────┘ ┴└──────┘ ┴ └───┘ ┴
src └───────┘ └──────┘ └───┘ ┴
typ └───────┘ ┴└──────┘ ┴ └───┘ ┴
doc └───┘
240 cseval t (add_const k.to_znum e) = k + cseval t e :=
id └────┘ ┴ └───────┘ ┴└──────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
src └────┘ └───────┘ └──────┘ ┴ ┴ └────┘
typ └────┘ ┴ └───────┘ ┴└──────┘ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
doc └────┘ └────┘
241 begin
st └─────
242 simp [add_const],
id └───────┘
src └────┘└───────┘┴
typ └────┘└───────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ─────────────────┘└─
243 cases k; simp! *,
id ┴
src └────┘ └─────┘
typ └────┘┴ └─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ ┴┴┴
st ─────────────────┘└─
244 simp [show znum.pos k ≠ 0, from dec_trivial],
id └──────┘ ┴ ┴ └─────────┘
src └────┘ ┴└──────┘┴ ┴┴└───────┘└─────────┘┴
typ └────┘ ┴└──────┘┴┴┴┴└───────┘└─────────┘┴
doc └────┘ ┴ ┴ ┴ └───────┘└─────────┘┴
txt └────┘ ┴ ┴ ┴ └───────┘ ┴
par └────┘ ┴ ┴ ┴ └───────┘ ┴
pid ┴┴ ┴ ┴ ┴ └───────┘ ┴
st ─────────────────────────────────────────────┘└─
245 induction e with n a x n b A B; simp *,
id ┴
src └────────┘ └─────────────────┘ └────┘
typ └────────┘┴└─────────────────┘ └────┘
doc └────────┘ └─────────────────┘ └────┘
txt └────────┘ └─────────────────┘ └────┘
par └────────┘ └─────────────────┘ └────┘
pid ┴ ┴└────────────────┘ ┴┴
st ───────────────────────────────────────┘└─
246 { rcases cs with ⟨n, rfl⟩,
id └┘
src └─────┘ └────────────┘
typ └─────┘└┘└────────────┘
doc └─────┘ └────────────┘
txt └─────┘ └────────────┘
par └─────┘ └────────────┘
pid ┴ └────────────┘
st ───┘└─────────────────────┘└─
247 refine ⟨⟨n + num.pos k, by simp; refl⟩, _⟩,
id ┴ ┴ └─────┘ ┴
src └─────┘ ┴┴┴└─────┘┴ └┘ ┴└──┘└┘└──┘└───┘
typ └─────┘ ┴┴┴┴└─────┘┴┴└┘ ┴└──┘└┘└──┘└───┘
doc └─────┘ ┴ ┴ ┴ └┘ ┴└──┘└┘└──┘└───┘
txt └─────┘ ┴ ┴ ┴ └┘ ┴└──┘└┘└──┘└───┘
par └─────┘ ┴ ┴ ┴ └┘ ┴└──┘└┘└──┘└───┘
pid ┴ ┴ ┴ ┴ └┘ └──────────────┘
st ─────────────────────────────┘└─────────┘└───┘└─
248 cases n; simp! },
id ┴
src └────┘ └────┘
typ └────┘┴ └────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴ ┴┴
st ──────────────────┘└┘└
249 { rcases B cs.2 with ⟨csb, h⟩, simp! [*, cs.1],
id ┴ └┘ └┘
src └─────┘ ┴ └──────────────┘ └────────┘ └─┘
typ └─────┘┴┴└┘└──────────────┘ └────────┘└┘└─┘
doc └─────┘ ┴ └──────────────┘ └────────┘ └─┘
txt └─────┘ ┴ └──────────────┘ └────────┘ └─┘
par └─────┘ ┴ └──────────────┘ └────────┘ └─┘
pid ┴ ┴ └──────────────┘ ┴┴└──┘ └─┘
st ──────────────────────────────┘└───────────────┘└─
250 rw [← tactic.ring.horner_add_const, add_comm], refl }
id └──────────────────────────┘ └──────┘
src └────┘└──────────────────────────┘└┘└──────┘┴ └───┘
typ └────┘└──────────────────────────┘└┘└──────┘┴ └───┘
doc └────┘ └┘ ┴ └───┘
txt └────┘ └┘ ┴ └───┘
par └────┘ └┘ ┴ └───┘
pid └──┘ └┘ ┴ ┴
st ─────────────────────────────────────┘└────────┘┴└─────┘└─
251 end
st ──┘
252
253 theorem cseval_horner' {α} [comm_semiring α] (t : tree α)
id └───────────┘ ┴ └──┘ ┴
src └───────────┘ └──┘
typ └───────────┘ ┴ └──┘ ┴
254 (a x n b) (h₁ : is_cs a) (h₂ : is_cs b) :
id └───┘ ┴ └───┘ ┴
src └───┘ └───┘
typ └───┘ ┴ └───┘ ┴
doc └───┘ └───┘
255 (horner' a x n b).is_cs ∧ cseval t (horner' a x n b) =
id └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ └───┘ ┴ └────┘ └─────┘ ┴
typ └─────┘ ┴ ┴ ┴ ┴ └───┘ ┴ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴
doc └─────┘ └───┘ └────┘ └─────┘
256 tactic.ring.horner (cseval t a) (t.get_or_zero x) n (cseval t b) :=
id └────────────────┘ └────┘ ┴ ┴ ┴└──────────┘ ┴ ┴ └────┘ ┴ ┴
src └────────────────┘ └────┘ └──────────┘ └────┘
typ └────────────────┘ └────┘ ┴ ┴ ┴└──────────┘ ┴ ┴ └────┘ ┴ ┴
doc └────┘ └──────────┘ └────┘
257 begin
st └─────
258 cases a with n₁ a₁ x₁ n₁ b₁; simp [horner']; split_ifs,
id ┴ └─────┘
src └────┘ └──────────────────┘ └────┘└─────┘┴ └───────┘
typ └────┘┴└──────────────────┘ └────┘└─────┘┴ └───────┘
doc └────┘ └──────────────────┘ └────┘└─────┘┴ └───────┘
txt └────┘ └──────────────────┘ └────┘ ┴ └───────┘
par └────┘ └──────────────────┘ └────┘ ┴ └───────┘
pid ┴ └──────────────────┘ ┴┴ ┴
st ───────────────────────────────────────────────────────┘└─
259 { simp! [*, tactic.ring.horner] },
id └────────────────┘
src └────────┘└────────────────┘└┘
typ └────────┘└────────────────┘└┘
doc └────────┘ └┘
txt └────────┘ └┘
par └────────┘ └┘
pid ┴┴└──┘ ┴┴
st ───┘└────────────────────────────┘└┘└
260 { exact ⟨⟨h₁, h₂⟩, rfl⟩ },
id └┘ └┘ └─┘
src └────┘ └┘ └─┘└─┘└┘
typ └────┘ └┘└┘└┘└─┘└─┘└┘
doc └────┘ └┘ └─┘ └┘
txt └────┘ └┘ └─┘ └┘
par └────┘ └┘ └─┘ └┘
pid ┴ └┘ └─┘ ┴┴
st ───┘└────────────────────┘└┘└
261 { refine ⟨⟨h₁.1, h₂⟩, eq.symm _⟩, simp! *,
id └┘ └┘ └─────┘
src └─────┘ └──┘ └─┘└─────┘└─┘ └─────┘
typ └─────┘ └┘└──┘└┘└─┘└─────┘└─┘ └─────┘
doc └─────┘ └──┘ └─┘ └─┘ └─────┘
txt └─────┘ └──┘ └─┘ └─┘ └─────┘
par └─────┘ └──┘ └─┘ └─┘ └─────┘
pid ┴ └──┘ └─┘ └─┘ ┴┴┴
st ───┘└────────────────────────────┘└───────┘└─
262 apply tactic.ring.horner_horner, simp },
id └───────────────────────┘
src └────┘└───────────────────────┘ └───┘
typ └────┘└───────────────────────┘ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st ──────────────────────────────────┘└─────┘└┘└
263 { exact ⟨⟨h₁, h₂⟩, rfl⟩ }
id └┘ └┘ └─┘
src └────┘ └┘ └─┘└─┘└┘
typ └────┘ └┘└┘└┘└─┘└─┘└┘
doc └────┘ └┘ └─┘ └┘
txt └────┘ └┘ └─┘ └┘
par └────┘ └┘ └─┘ └┘
pid ┴ └┘ └─┘ ┴┴
st ─────────────────────────┘└─
264 end
st ──┘
265
266 theorem cseval_add {α} [comm_semiring α] (t : tree α)
id └───────────┘ ┴ └──┘ ┴
src └───────────┘ └──┘
typ └───────────┘ ┴ └──┘ ┴
267 {e₁ e₂ : horner_expr} (cs₁ : e₁.is_cs) (cs₂ : e₂.is_cs) :
id └─────────┘ └┘└────┘ └┘└────┘
src └─────────┘ └────┘ └────┘
typ └─────────┘ └┘└────┘ └┘└────┘
doc └─────────┘ └────┘ └────┘
268 (add e₁ e₂).is_cs ∧
id └─┘ └┘ └┘ └───┘ ┴
src └─┘ └───┘ ┴
typ └─┘ └┘ └┘ └───┘ ┴
doc └───┘
269 cseval t (add e₁ e₂) = cseval t e₁ + cseval t e₂ :=
id └────┘ ┴ └─┘ └┘ └┘ ┴ └────┘ ┴ └┘ ┴ └────┘ ┴ └┘
src └────┘ └─┘ ┴ └────┘ ┴ └────┘
typ └────┘ ┴ └─┘ └┘ └┘ ┴ └────┘ ┴ └┘ ┴ └────┘ ┴ └┘
doc └────┘ └────┘ └────┘
270 begin
st └─────
271 induction e₁ with n₁ a₁ x₁ n₁ b₁ A₁ B₁ generalizing e₂; simp!,
id └┘
src └────────┘ └────────────────────────────────────────┘ └───┘
typ └────────┘└┘└────────────────────────────────────────┘ └───┘
doc └────────┘ └────────────────────────────────────────┘ └───┘
txt └────────┘ └────────────────────────────────────────┘ └───┘
par └────────┘ └────────────────────────────────────────┘ └───┘
pid ┴ ┴└───────────────────────┘└──────────────┘ ┴
st ──────────────────────────────────────────────────────────────┘└─
272 { rcases cs₁ with ⟨n₁, rfl⟩,
id └─┘
src └─────┘ └─────────────┘
typ └─────┘└─┘└─────────────┘
doc └─────┘ └─────────────┘
txt └─────┘ └─────────────┘
par └─────┘ └─────────────┘
pid ┴ └─────────────┘
st ───┘└───────────────────────┘└─
273 simpa using cseval_add_const t n₁ cs₂ },
id └──────────────┘ ┴ └┘ └─┘
src └──────────┘└──────────────┘┴ ┴ ┴ ┴
typ └──────────┘└──────────────┘┴┴┴└┘┴└─┘┴
doc └──────────┘ ┴ ┴ ┴ ┴
txt └──────────┘ ┴ ┴ ┴ ┴
par └──────────┘ ┴ ┴ ┴ ┴
pid ┴└────┘ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────┘└┘└
274 induction e₂ with n₂ a₂ x₂ n₂ b₂ A₂ B₂ generalizing n₁ b₁,
id └┘
src └────────┘ └───────────────────────────────────────────┘
typ └────────┘└┘└───────────────────────────────────────────┘
doc └────────┘ └───────────────────────────────────────────┘
txt └────────┘ └───────────────────────────────────────────┘
par └────────┘ └───────────────────────────────────────────┘
pid ┴ ┴└───────────────────────┘└─────────────────┘
st ──────────────────────────────────────────────────────────┘└─
275 { rcases cs₂ with ⟨n₂, rfl⟩,
id └─┘
src └─────┘ └─────────────┘
typ └─────┘└─┘└─────────────┘
doc └─────┘ └─────────────┘
txt └─────┘ └─────────────┘
par └─────┘ └─────────────┘
pid ┴ └─────────────┘
st ───┘└───────────────────────┘└─
276 simp! [cseval_add_const t n₂ cs₁] },
id └──────────────┘ ┴ └┘ └─┘
src └─────┘└──────────────┘┴ ┴ ┴ └┘
typ └─────┘└──────────────┘┴┴┴└┘┴└─┘└┘
doc └─────┘ ┴ ┴ ┴ └┘
txt └─────┘ ┴ ┴ ┴ └┘
par └─────┘ ┴ ┴ ┴ └┘
pid ┴┴┴ ┴ ┴ ┴ ┴┴
st ─────────────────────────────────────┘└┘└
277 cases cs₁ with csa₁ csb₁, cases id cs₂ with csa₂ csb₂,
id └─┘ └┘ └─┘
src └────┘ └─────────────┘ └────┘└┘┴ └─────────────┘
typ └────┘└─┘└─────────────┘ └────┘└┘┴└─┘└─────────────┘
doc └────┘ └─────────────┘ └────┘ ┴ └─────────────┘
txt └────┘ └─────────────┘ └────┘ ┴ └─────────────┘
par └────┘ └─────────────┘ └────┘ ┴ └─────────────┘
pid ┴ └─────────────┘ ┴ ┴ └─────────────┘
st ─────────────────────────┘└───────────────────────────┘└─
278 simp!, have C := pos_num.cmp_to_nat x₁ x₂,
id └────────────────┘ └┘ └┘
src └───┘ └────────┘└────────────────┘┴ ┴
typ └───┘ └────────┘└────────────────┘┴└┘┴└┘
doc └───┘ └────────┘ ┴ ┴
txt └───┘ └────────┘ ┴ ┴
par └───┘ └────────┘ ┴ ┴
pid ┴ └────┘┴└─┘ ┴ ┴
st ──────┘└──────────────────────────────────┘└─
279 cases pos_num.cmp x₁ x₂; simp!,
id └─────────┘ └┘ └┘
src └────┘└─────────┘┴ ┴ └───┘
typ └────┘└─────────┘┴└┘┴└┘ └───┘
doc └────┘ ┴ ┴ └───┘
txt └────┘ ┴ ┴ └───┘
par └────┘ ┴ ┴ └───┘
pid ┴ ┴ ┴ ┴
st ───────────────────────────────┘└─
280 { rcases B₁ csb₁ cs₂ with ⟨csh, h⟩,
id └┘ └──┘ └─┘
src └─────┘ ┴ ┴ └────────────┘
typ └─────┘└┘┴└──┘┴└─┘└────────────┘
doc └─────┘ ┴ ┴ └────────────┘
txt └─────┘ ┴ ┴ └────────────┘
par └─────┘ ┴ ┴ └────────────┘
pid ┴ ┴ ┴ └────────────┘
st ───┘└──────────────────────────────┘└─
281 refine ⟨⟨csa₁, csh⟩, eq.symm _⟩,
id └──┘ └─┘ └─────┘
src └─────┘ └┘ └─┘└─────┘└─┘
typ └─────┘ └──┘└┘└─┘└─┘└─────┘└─┘
doc └─────┘ └┘ └─┘ └─┘
txt └─────┘ └┘ └─┘ └─┘
par └─────┘ └┘ └─┘ └─┘
pid ┴ └┘ └─┘ └─┘
st ──────────────────────────────────┘└─
282 apply tactic.ring.horner_add_const,
id └──────────────────────────┘
src └────┘└──────────────────────────┘
typ └────┘└──────────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────────────┘└─
283 exact h.symm },
id └────┘
src └────┘└────┘┴
typ └────┘└────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────┘└┘└
284 { cases C,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───┘└─────┘└─
285 have B0 : is_cs 0 → ∀ {e₂ : horner_expr}, is_cs e₂ →
id └───┘ └─────────┘
src └────────┘ └─┘ ┴ └─────┘└─────────┘┴ ┴ ┴ ┴ └
typ └────────┘└───┘└─┘ ┴ └─────┘└─────────┘┴ ┴ ┴ ┴ └
doc └────────┘ └─┘ ┴ └─────┘└─────────┘┴ ┴ ┴ ┴ └
txt └────────┘ └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └
par └────────┘ └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └
pid └─────┘└─┘ └─┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └
st ─────────────────────────────────────────────────────────
286 is_cs (add 0 e₂) ∧ cseval t (add 0 e₂) = cseval t 0 + cseval t e₂ :=
id └───┘ └─┘ ┴ ┴ └────┘ ┴
src ─────┘└───┘┴ └─┘ └┘ ┴ ┴ ┴ └─┘└─┘ └┘┴┴ ┴ └─┘┴┴└────┘┴ ┴ └───
typ ─────┘└───┘┴ └─┘ └┘ ┴ ┴ ┴ └─┘└─┘ └┘┴┴ ┴ └─┘┴┴└────┘┴┴┴ └───
doc ─────┘└───┘┴ └─┘ └┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └─┘ ┴└────┘┴ ┴ └───
txt ─────┘ ┴ └─┘ └┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ └───
par ─────┘ ┴ └─┘ └┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ └───
pid ─────┘ ┴ └─┘ └┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └─┘ ┴ ┴ ┴ └───
st ───────────────────────────────────────────────────────────────────────────
287 λ _ e₂ c, ⟨c, (zero_add _).symm⟩,
id └──────┘
src ─────┘ └───────┘ └┘ └──────┘└───────┘
typ ─────┘ └───────┘ └┘ └──────┘└───────┘
doc ─────┘ └───────┘ └┘ └───────┘
txt ─────┘ └───────┘ └┘ └───────┘
par ─────┘ └───────┘ └┘ └───────┘
pid ─────┘ └───────┘ └┘ └───────┘
st ─────────────────────────────────────┘└─
288 cases e : num.sub' n₁ n₂ with k k; simp!,
id └──────┘ └┘ └┘
src └────┘ └─┘└──────┘┴ ┴ └───────┘ └───┘
typ └────┘ └─┘└──────┘┴└┘┴└┘└───────┘ └───┘
doc └────┘ └─┘ ┴ ┴ └───────┘ └───┘
txt └────┘ └─┘ ┴ ┴ └───────┘ └───┘
par └────┘ └─┘ ┴ ┴ └───────┘ └───┘
pid ┴ └─┘ ┴ ┴ └───────┘ ┴
st ────────────────────────────────────────────┘└─
289 { have : n₁ = n₂,
id └┘ └┘
src └─────┘ ┴ ┴
typ └─────┘└┘┴ ┴└┘
doc └─────┘ ┴ ┴
txt └─────┘ ┴ ┴
par └─────┘ ┴ ┴
pid └───┘└┘ ┴ ┴
st ─────┘└────────────┘└─
290 { have := congr_arg (coe : znum → ℤ) e,
id └───────┘ └─┘ └──┘ ┴
src └──────┘└───────┘┴ └─┘└─┘└──┘┴ ┴ └┘
typ └──────┘└───────┘┴ └─┘└─┘└──┘┴ ┴ └┘┴
doc └──────┘ ┴ └─┘└──┘┴ ┴ └┘
txt └──────┘ ┴ └─┘ ┴ ┴ └┘
par └──────┘ ┴ └─┘ ┴ ┴ └┘
pid └───┘└─┘ ┴ └─┘ ┴ ┴ └┘
st ───────┘└──────────────────────────────────┘└─
291 simp at this,
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└─────┘
st ───────────────────┘└─
292 have := sub_eq_zero.1 this,
id └─────────┘ └──┘
src └──────┘└─────────┘└─┘
typ └──────┘└─────────┘└─┘└──┘
doc └──────┘ └─┘
txt └──────┘ └─┘
par └──────┘ └─┘
pid └───┘└─┘ └─┘
st ─────────────────────────────────┘└─
293 rw [← num.to_nat_to_int, ← num.to_nat_to_int] at this,
id └───────────────┘ └───────────────┘
src └────┘└───────────────┘└──┘└───────────────┘└───────┘
typ └────┘└───────────────┘└──┘└───────────────┘└───────┘
doc └────┘ └──┘ └───────┘
txt └────┘ └──┘ └───────┘
par └────┘ └──┘ └───────┘
pid └──┘ └──┘ ┴└──────┘
st ──────────────────────────────┘└───────────────────┘┴└──────┘└─
294 exact num.to_nat_inj.1 (int.coe_nat_inj this) },
id └────────────┘ └─────────────┘ └──┘
src └────┘└────────────┘└─┘ └─────────────┘┴ └┘
typ └────┘└────────────┘└─┘ └─────────────┘┴└──┘└┘
doc └────┘ └─┘ ┴ └┘
txt └────┘ └─┘ ┴ └┘
par └────┘ └─┘ ┴ └┘
pid ┴ └─┘ ┴ ┴┴
st ─────────────────────────────────────────────────────┘└┘└
295 subst n₂,
id └┘
src └────┘
typ └────┘└┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────┘└─
296 rcases cseval_horner' _ _ _ _ _ _ _ with ⟨csh, h⟩,
id └────────────┘
src └─────┘└────────────┘└──────────────────────────┘
typ └─────┘└────────────┘└──────────────────────────┘
doc └─────┘ └──────────────────────────┘
txt └─────┘ └──────────────────────────┘
par └─────┘ └──────────────────────────┘
pid ┴ └──────────────────────────┘
st ──────────────────────────────────────────────────────┘└─
297 { refine ⟨csh, h.trans (eq.symm _)⟩,
id └─┘ └─────┘ └─────┘
src └─────┘ └┘└─────┘┴ └─────┘└──┘
typ └─────┘ └─┘└┘└─────┘┴ └─────┘└──┘
doc └─────┘ └┘ ┴ └──┘
txt └─────┘ └┘ ┴ └──┘
par └─────┘ └┘ ┴ └──┘
pid ┴ └┘ ┴ └──┘
st ───────┘└───────────────────────────────┘└─
298 simp *,
src └────┘
typ └────┘
doc └────┘
txt └────┘
par └────┘
pid ┴┴
st ─────────────┘└─
299 apply tactic.ring.horner_add_horner_eq; try {refl},
id └──────────────────────────────┘
src └────┘└──────────────────────────────┘ └───┘└──┘┴
typ └────┘└──────────────────────────────┘ └───┘└──┘┴
doc └────┘ └───┘└──┘┴
txt └────┘ └───┘└──┘┴
par └────┘ └───┘└──┘┴
pid ┴ └─────┘
st ────────────────────────────────────────────────────┘└──┘└┘└
300 simp },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ────────────┘└┘└
301 all_goals {simp! *} },
src └─────────┘└─────┘└┘
typ └─────────┘└─────┘└┘
doc └─────────┘└─────┘└┘
txt └─────────┘└─────┘└┘
par └─────────┘└─────┘└┘
pid └────────┘┴
st ────────────────┘└─────┘┴┴└┘└
302 { simp [B₁ csb₁ csb₂],
id └┘ └──┘ └──┘
src └────┘ ┴ ┴ ┴
typ └────┘└┘┴└──┘┴└──┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴┴ ┴ ┴ ┴
st ─────┘└─────────────────┘└─
303 rcases A₂ csa₂ _ _ B0 ⟨csa₁, 0, rfl⟩ with ⟨csh, h⟩,
id └┘ └──┘ └┘ └──┘ └─┘
src └─────┘ ┴ └───┘ ┴ └───┘└─┘└─────────────┘
typ └─────┘└┘┴└──┘└───┘└┘┴ └──┘└───┘└─┘└─────────────┘
doc └─────┘ ┴ └───┘ ┴ └───┘ └─────────────┘
txt └─────┘ ┴ └───┘ ┴ └───┘ └─────────────┘
par └─────┘ ┴ └───┘ ┴ └───┘ └─────────────┘
pid ┴ ┴ └───┘ ┴ └───┘ └─────────────┘
st ───────────────────────────────────────────────────────┘└─
304 refine ⟨csh, eq.symm _⟩,
id └─┘ └─────┘
src └─────┘ └┘└─────┘└─┘
typ └─────┘ └─┘└┘└─────┘└─┘
doc └─────┘ └┘ └─┘
txt └─────┘ └┘ └─┘
par └─────┘ └┘ └─┘
pid ┴ └┘ └─┘
st ────────────────────────────┘└─
305 rw [show id = add 0, from rfl, h],
id └┘ ┴ └─┘ └─┘ ┴
src └──┘ ┴└┘┴ ┴└─┘└───────┘└─┘└┘ ┴
typ └──┘ ┴└┘┴┴┴└─┘└───────┘└─┘└┘┴┴
doc └──┘ ┴ ┴ ┴ └───────┘ └┘ ┴
txt └──┘ ┴ ┴ ┴ └───────┘ └┘ ┴
par └──┘ ┴ ┴ ┴ └───────┘ └┘ ┴
pid └┘ ┴ ┴ ┴ └───────┘ └┘ ┴
st ──────────────────────────────────┘└─┘└──
306 apply tactic.ring.horner_add_horner_gt,
id └──────────────────────────────┘
src └────┘└──────────────────────────────┘
typ └────┘└──────────────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ───────────────────────────────────────────┘└─
307 { change (_ + k : ℕ) = _,
id ┴ ┴
src └─────┘ └┘┴┴ └─┘ └┘ └┘
typ └─────┘ └┘┴┴┴└─┘ └┘ └┘
doc └─────┘ └┘ ┴ └─┘ └┘ └┘
txt └─────┘ └┘ ┴ └─┘ └┘ └┘
par └─────┘ └┘ ┴ └─┘ └┘ └┘
pid ┴ └┘ ┴ └─┘ └┘ └┘
st ───────┘└────────────────────┘└─
308 rw [← int.coe_nat_inj', int.coe_nat_add,
id └──────────────┘ └─────────────┘
src └────┘└──────────────┘└┘└─────────────┘└─
typ └────┘└──────────────┘└┘└─────────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid └──┘ └┘ └─
st ─────────────────────────────┘└───────────────┘└─
309 eq_comm, ← sub_eq_iff_eq_add'],
id └─────┘ └────────────────┘
src ─────────┘└─────┘└──┘└────────────────┘┴
typ ─────────┘└─────┘└──┘└────────────────┘┴
doc ─────────┘ └──┘ ┴
txt ─────────┘ └──┘ ┴
par ─────────┘ └──┘ ┴
pid ─────────┘ └──┘ ┴
st ────────────────┘└────────────────────┘└──
310 simpa using congr_arg (coe : znum → ℤ) e },
id └───────┘ └─┘ └──┘ ┴
src └──────────┘└───────┘┴ └─┘└─┘└──┘┴ ┴ └┘ ┴
typ └──────────┘└───────┘┴ └─┘└─┘└──┘┴ ┴ └┘┴┴
doc └──────────┘ ┴ └─┘└──┘┴ ┴ └┘ ┴
txt └──────────┘ ┴ └─┘ ┴ ┴ └┘ ┴
par └──────────┘ ┴ └─┘ ┴ ┴ └┘ ┴
pid ┴└────┘ ┴ └─┘ ┴ ┴ └┘ ┴
st ────────────────────────────────────────────────┘└┘└
311 all_goals { apply add_comm } },
id └──────┘
src └──────────┘└────┘└──────┘┴└┘
typ └──────────┘└────┘└──────┘┴└┘
doc └──────────┘└────┘ ┴└┘
txt └──────────┘└────┘ ┴└┘
par └──────────┘└────┘ ┴└┘
pid └───────┘ └┘┴
st ────────────────┘└──────────────┘┴┴└┘└
312 { have : (horner a₂ x₁ (num.pos k) 0).is_cs := ⟨csa₂, 0, rfl⟩,
id └────┘ └┘ └┘ └─────┘ ┴ └──┘ └─┘
src └─────┘ └────┘┴ ┴ ┴ └─────┘┴ └────────────┘ └───┘└─┘┴
typ └─────┘ └────┘┴└┘┴└┘┴ └─────┘┴┴└────────────┘ └──┘└───┘└─┘┴
doc └─────┘ ┴ ┴ ┴ ┴ └────────────┘ └───┘ ┴
txt └─────┘ ┴ ┴ ┴ ┴ └────────────┘ └───┘ ┴
par └─────┘ ┴ ┴ ┴ ┴ └────────────┘ └───┘ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ └───────┘└───┘ └───┘ ┴
st ────────────────────────────────────────────────────────────────┘└─
313 simp [B₁ csb₁ csb₂, A₁ csa₁ this],
id └┘ └──┘ └──┘ └┘ └──┘ └──┘
src └────┘ ┴ ┴ └┘ ┴ ┴ ┴
typ └────┘└┘┴└──┘┴└──┘└┘└┘┴└──┘┴└──┘┴
doc └────┘ ┴ ┴ └┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ └┘ ┴ ┴ ┴
par └────┘ ┴ ┴ └┘ ┴ ┴ ┴
pid ┴┴ ┴ ┴ └┘ ┴ ┴ ┴
st ──────────────────────────────────────┘└─
314 symmetry, apply tactic.ring.horner_add_horner_lt,
id └──────────────────────────────┘
src └──────┘ └────┘└──────────────────────────────┘
typ └──────┘ └────┘└──────────────────────────────┘
doc └──────┘ └────┘
txt └──────┘ └────┘
par └──────┘ └────┘
pid ┴
st ─────────────┘└──────────────────────────────────────┘└─
315 { change (_ + k : ℕ) = _,
id ┴
src └─────┘ └┘ ┴ └─┘ └┘ └┘
typ └─────┘ └┘ ┴┴└─┘ └┘ └┘
doc └─────┘ └┘ ┴ └─┘ └┘ └┘
txt └─────┘ └┘ ┴ └─┘ └┘ └┘
par └─────┘ └┘ ┴ └─┘ └┘ └┘
pid ┴ └┘ ┴ └─┘ └┘ └┘
st ───────┘└────────────────────┘└─
316 rw [← int.coe_nat_inj', int.coe_nat_add,
id └──────────────┘ └─────────────┘
src └────┘└──────────────┘└┘└─────────────┘└─
typ └────┘└──────────────┘└┘└─────────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid └──┘ └┘ └─
st ───────────────────────────────┘└───────────────┘└─
317 eq_comm, ← sub_eq_iff_eq_add', ← neg_inj', neg_sub],
id └─────┘ └────────────────┘ └──────┘ └─────┘
src ───────────┘└─────┘└──┘└────────────────┘└──┘└──────┘└┘└─────┘┴
typ ───────────┘└─────┘└──┘└────────────────┘└──┘└──────┘└┘└─────┘┴
doc ───────────┘ └──┘ └──┘ └┘ ┴
txt ───────────┘ └──┘ └──┘ └┘ ┴
par ───────────┘ └──┘ └──┘ └┘ ┴
pid ───────────┘ └──┘ └──┘ └┘ ┴
st ──────────────────┘└────────────────────┘└──────────┘└───────┘└──
318 simpa using congr_arg (coe : znum → ℤ) e },
id └───────┘ └─┘ └──┘ ┴
src └──────────┘└───────┘┴ └─┘└─┘└──┘┴ ┴ └┘ ┴
typ └──────────┘└───────┘┴ └─┘└─┘└──┘┴ ┴ └┘┴┴
doc └──────────┘ ┴ └─┘└──┘┴ ┴ └┘ ┴
txt └──────────┘ ┴ └─┘ ┴ ┴ └┘ ┴
par └──────────┘ ┴ └─┘ ┴ ┴ └┘ ┴
pid ┴└────┘ ┴ └─┘ ┴ ┴ └┘ ┴
st ────────────────────────────────────────────────┘└┘└
319 { refl }, { apply add_comm } } },
id └──────┘
src └───┘ └────┘└──────┘┴
typ └───┘ └────┘└──────┘┴
doc └───┘ └────┘ ┴
txt └───┘ └────┘ ┴
par └───┘ └────┘ ┴
pid ┴ ┴ ┴
st ───────┘└───┘└┘└────────────────┘└────┘└
320 { rcases B₂ csb₂ _ _ B₁ ⟨csa₁, csb₁⟩ with ⟨csh, h⟩,
id └┘ └──┘ └┘ └──┘ └──┘
src └─────┘ ┴ └───┘ ┴ └┘ └─────────────┘
typ └─────┘└┘┴└──┘└───┘└┘┴ └──┘└┘└──┘└─────────────┘
doc └─────┘ ┴ └───┘ ┴ └┘ └─────────────┘
txt └─────┘ ┴ └───┘ ┴ └┘ └─────────────┘
par └─────┘ ┴ └───┘ ┴ └┘ └─────────────┘
pid ┴ ┴ └───┘ ┴ └┘ └─────────────┘
st ───────────────────────────────────────────────────┘└─
321 refine ⟨⟨csa₂, csh⟩, eq.symm _⟩,
id └──┘ └─┘ └─────┘
src └─────┘ └┘ └─┘└─────┘└─┘
typ └─────┘ └──┘└┘└─┘└─┘└─────┘└─┘
doc └─────┘ └┘ └─┘ └─┘
txt └─────┘ └┘ └─┘ └─┘
par └─────┘ └┘ └─┘ └─┘
pid ┴ └┘ └─┘ └─┘
st ──────────────────────────────────┘└─
322 apply tactic.ring.const_add_horner,
id └──────────────────────────┘
src └────┘└──────────────────────────┘
typ └────┘└──────────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────────────┘└─
323 simp [h] }
id ┴
src └────┘ └┘
typ └────┘┴└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ────────────┘└─
324 end
st ──┘
325
326 theorem cseval_mul_const {α} [comm_semiring α] (t : tree α)
id └───────────┘ ┴ └──┘ ┴
src └───────────┘ └──┘
typ └───────────┘ ┴ └──┘ ┴
327 (k : num) {e : horner_expr} (cs : e.is_cs) :
id └─┘ └─────────┘ ┴└────┘
src └─┘ └─────────┘ └────┘
typ └─┘ └─────────┘ ┴└────┘
doc └─┘ └─────────┘ └────┘
328 (mul_const k.to_znum e).is_cs ∧
id └───────┘ ┴└──────┘ ┴ └───┘ ┴
src └───────┘ └──────┘ └───┘ ┴
typ └───────┘ ┴└──────┘ ┴ └───┘ ┴
doc └───┘
329 cseval t (mul_const k.to_znum e) = cseval t e * k :=
id └────┘ ┴ └───────┘ ┴└──────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
src └────┘ └───────┘ └──────┘ ┴ └────┘ ┴
typ └────┘ ┴ └───────┘ ┴└──────┘ ┴ ┴ └────┘ ┴ ┴ ┴ ┴
doc └────┘ └────┘
330 begin
st └─────
331 simp [mul_const],
id └───────┘
src └────┘└───────┘┴
typ └────┘└───────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ─────────────────┘└─
332 split_ifs with h h,
src └────────────────┘
typ └────────────────┘
doc └────────────────┘
txt └────────────────┘
par └────────────────┘
pid ┴└──────┘
st ───────────────────┘└─
333 { cases (num.to_znum_inj.1 h : k = 0),
id └─────────────┘ ┴ ┴ ┴
src └────┘ └─────────────┘└─┘ └─┘ ┴┴└─┘
typ └────┘ └─────────────┘└─┘┴└─┘┴┴┴└─┘
doc └────┘ └─┘ └─┘ ┴ └─┘
txt └────┘ └─┘ └─┘ ┴ └─┘
par └────┘ └─┘ └─┘ ┴ └─┘
pid ┴ └─┘ └─┘ ┴ └─┘
st ───┘└─────────────────────────────────┘└─
334 exact ⟨⟨0, rfl⟩, (mul_zero _).symm⟩ },
id └─┘ └──────┘
src └────┘ └─┘└─┘└─┘ └──────┘└────────┘
typ └────┘ └─┘└─┘└─┘ └──────┘└────────┘
doc └────┘ └─┘ └─┘ └────────┘
txt └────┘ └─┘ └─┘ └────────┘
par └────┘ └─┘ └─┘ └────────┘
pid ┴ └─┘ └─┘ └───────┘┴
st ───────────────────────────────────────┘└┘└
335 { cases (num.to_znum_inj.1 h : k = 1),
id └─────────────┘ ┴ ┴
src └────┘ └─────────────┘└─┘ └─┘ ┴ └─┘
typ └────┘ └─────────────┘└─┘┴└─┘┴┴ └─┘
doc └────┘ └─┘ └─┘ ┴ └─┘
txt └────┘ └─┘ └─┘ ┴ └─┘
par └────┘ └─┘ └─┘ ┴ └─┘
pid ┴ └─┘ └─┘ ┴ └─┘
st ───┘└─────────────────────────────────┘└─
336 exact ⟨cs, (mul_one _).symm⟩ },
id └┘ └─────┘
src └────┘ └┘ └─────┘└────────┘
typ └────┘ └┘└┘ └─────┘└────────┘
doc └────┘ └┘ └────────┘
txt └────┘ └┘ └────────┘
par └────┘ └┘ └────────┘
pid ┴ └┘ └───────┘┴
st ────────────────────────────────┘└┘└
337 induction e with n a x n b A B; simp *,
id ┴
src └────────┘ └─────────────────┘ └────┘
typ └────────┘┴└─────────────────┘ └────┘
doc └────────┘ └─────────────────┘ └────┘
txt └────────┘ └─────────────────┘ └────┘
par └────────┘ └─────────────────┘ └────┘
pid ┴ ┴└────────────────┘ ┴┴
st ───────────────────────────────────────┘└─
338 { rcases cs with ⟨n, rfl⟩,
id └┘
src └─────┘ └────────────┘
typ └─────┘└┘└────────────┘
doc └─────┘ └────────────┘
txt └─────┘ └────────────┘
par └─────┘ └────────────┘
pid ┴ └────────────┘
st ───┘└─────────────────────┘└─
339 suffices, refine ⟨⟨n * k, this⟩, _⟩,
id ┴ ┴ ┴ └──┘
src └──────┘ └─────┘ ┴┴┴ └┘ └───┘
typ └──────┘ └─────┘ ┴┴┴┴┴└┘└──┘└───┘
doc └──────┘ └─────┘ ┴ ┴ └┘ └───┘
txt └──────┘ └─────┘ ┴ ┴ └┘ └───┘
par └──────┘ └─────┘ ┴ ┴ └┘ └───┘
pid └──────┘ ┴ ┴ ┴ └┘ └───┘
st ───────────┘└─────────────────────────┘└─
340 swap, {cases n; cases k; refl},
id ┴ ┴
src └──┘ └────┘ └────┘ └──┘
typ └──┘ └────┘┴ └────┘┴ └──┘
doc └──┘ └────┘ └────┘ └──┘
txt └──┘ └────┘ └────┘ └──┘
par └──┘ └────┘ └────┘ └──┘
pid ┴ ┴
st ───────┘└───────────────────────┘└┘└
341 rw [show _, from this], simp! },
id └──┘
src └──┘ └───────┘ ┴ └────┘
typ └──┘ └───────┘└──┘┴ └────┘
doc └──┘ └───────┘ ┴ └────┘
txt └──┘ └───────┘ ┴ └────┘
par └──┘ └───────┘ ┴ └────┘
pid └┘ └───────┘ ┴ ┴┴
st ────────────────────────┘└───────┘└┘└
342 { cases cs, simp! *,
id └┘
src └────┘ └─────┘
typ └────┘└┘ └─────┘
doc └────┘ └─────┘
txt └────┘ └─────┘
par └────┘ └─────┘
pid ┴ ┴┴┴
st ───────────┘└───────┘└─
343 symmetry, apply tactic.ring.horner_mul_const; refl }
id └──────────────────────────┘
src └──────┘ └────┘└──────────────────────────┘ └───┘
typ └──────┘ └────┘└──────────────────────────┘ └───┘
doc └──────┘ └────┘ └───┘
txt └──────┘ └────┘ └───┘
par └──────┘ └────┘ └───┘
pid ┴ ┴
st ───────────┘└─────────────────────────────────────────┘└─
344 end
st ──┘
345
346 theorem cseval_mul {α} [comm_semiring α] (t : tree α)
id └───────────┘ ┴ └──┘ ┴
src └───────────┘ └──┘
typ └───────────┘ ┴ └──┘ ┴
347 {e₁ e₂ : horner_expr} (cs₁ : e₁.is_cs) (cs₂ : e₂.is_cs) :
id └─────────┘ └┘└────┘ └┘└────┘
src └─────────┘ └────┘ └────┘
typ └─────────┘ └┘└────┘ └┘└────┘
doc └─────────┘ └────┘ └────┘
348 (mul e₁ e₂).is_cs ∧
id └─┘ └┘ └┘ └───┘ ┴
src └─┘ └───┘ ┴
typ └─┘ └┘ └┘ └───┘ ┴
doc └───┘
349 cseval t (mul e₁ e₂) = cseval t e₁ * cseval t e₂ :=
id └────┘ ┴ └─┘ └┘ └┘ ┴ └────┘ ┴ └┘ ┴ └────┘ ┴ └┘
src └────┘ └─┘ ┴ └────┘ ┴ └────┘
typ └────┘ ┴ └─┘ └┘ └┘ ┴ └────┘ ┴ └┘ ┴ └────┘ ┴ └┘
doc └────┘ └────┘ └────┘
350 begin
st └─────
351 induction e₁ with n₁ a₁ x₁ n₁ b₁ A₁ B₁ generalizing e₂; simp!,
id └┘
src └────────┘ └────────────────────────────────────────┘ └───┘
typ └────────┘└┘└────────────────────────────────────────┘ └───┘
doc └────────┘ └────────────────────────────────────────┘ └───┘
txt └────────┘ └────────────────────────────────────────┘ └───┘
par └────────┘ └────────────────────────────────────────┘ └───┘
pid ┴ ┴└───────────────────────┘└──────────────┘ ┴
st ──────────────────────────────────────────────────────────────┘└─
352 { rcases cs₁ with ⟨n₁, rfl⟩,
id └─┘
src └─────┘ └─────────────┘
typ └─────┘└─┘└─────────────┘
doc └─────┘ └─────────────┘
txt └─────┘ └─────────────┘
par └─────┘ └─────────────┘
pid ┴ └─────────────┘
st ───┘└───────────────────────┘└─
353 simpa [mul_comm] using cseval_mul_const t n₁ cs₂ },
id └──────┘ └──────────────┘ ┴ └┘ └─┘
src └─────┘└──────┘└──────┘└──────────────┘┴ ┴ ┴ ┴
typ └─────┘└──────┘└──────┘└──────────────┘┴┴┴└┘┴└─┘┴
doc └─────┘ └──────┘ ┴ ┴ ┴ ┴
txt └─────┘ └──────┘ ┴ ┴ ┴ ┴
par └─────┘ └──────┘ ┴ ┴ ┴ ┴
pid ┴┴ ┴┴└────┘ ┴ ┴ ┴ ┴
st ────────────────────────────────────────────────────┘└┘└
354 induction e₂ with n₂ a₂ x₂ n₂ b₂ A₂ B₂,
id └┘
src └────────┘ └────────────────────────┘
typ └────────┘└┘└────────────────────────┘
doc └────────┘ └────────────────────────┘
txt └────────┘ └────────────────────────┘
par └────────┘ └────────────────────────┘
pid ┴ ┴└───────────────────────┘
st ───────────────────────────────────────┘└─
355 { rcases cs₂ with ⟨n₂, rfl⟩,
id └─┘
src └─────┘ └─────────────┘
typ └─────┘└─┘└─────────────┘
doc └─────┘ └─────────────┘
txt └─────┘ └─────────────┘
par └─────┘ └─────────────┘
pid ┴ └─────────────┘
st ───┘└───────────────────────┘└─
356 simpa! using cseval_mul_const t n₂ cs₁ },
id └──────────────┘ ┴ └┘ └─┘
src └───────────┘└──────────────┘┴ ┴ ┴ ┴
typ └───────────┘└──────────────┘┴┴┴└┘┴└─┘┴
doc └───────────┘ ┴ ┴ ┴ ┴
txt └───────────┘ ┴ ┴ ┴ ┴
par └───────────┘ ┴ ┴ ┴ ┴
pid ┴┴└────┘ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────┘└┘└
357 cases cs₁ with csa₁ csb₁, cases id cs₂ with csa₂ csb₂,
id └─┘ └┘ └─┘
src └────┘ └─────────────┘ └────┘└┘┴ └─────────────┘
typ └────┘└─┘└─────────────┘ └────┘└┘┴└─┘└─────────────┘
doc └────┘ └─────────────┘ └────┘ ┴ └─────────────┘
txt └────┘ └─────────────┘ └────┘ ┴ └─────────────┘
par └────┘ └─────────────┘ └────┘ ┴ └─────────────┘
pid ┴ └─────────────┘ ┴ ┴ └─────────────┘
st ─────────────────────────┘└───────────────────────────┘└─
358 simp!, have C := pos_num.cmp_to_nat x₁ x₂,
id └────────────────┘ └┘ └┘
src └───┘ └────────┘└────────────────┘┴ ┴
typ └───┘ └────────┘└────────────────┘┴└┘┴└┘
doc └───┘ └────────┘ ┴ ┴
txt └───┘ └────────┘ ┴ ┴
par └───┘ └────────┘ ┴ ┴
pid ┴ └────┘┴└─┘ ┴ ┴
st ──────┘└──────────────────────────────────┘└─
359 cases A₂ csa₂ with csA₂ hA₂,
id └┘ └──┘
src └────┘ ┴ └────────────┘
typ └────┘└┘┴└──┘└────────────┘
doc └────┘ ┴ └────────────┘
txt └────┘ ┴ └────────────┘
par └────┘ ┴ └────────────┘
pid ┴ ┴ └────────────┘
st ────────────────────────────┘└─
360 cases pos_num.cmp x₁ x₂; simp!,
id └─────────┘ └┘ └┘
src └────┘└─────────┘┴ ┴ └───┘
typ └────┘└─────────┘┴└┘┴└┘ └───┘
doc └────┘ ┴ ┴ └───┘
txt └────┘ ┴ ┴ └───┘
par └────┘ ┴ ┴ └───┘
pid ┴ ┴ ┴ ┴
st ───────────────────────────────┘└─
361 { simp [A₁ csa₁ cs₂, B₁ csb₁ cs₂],
id └┘ └──┘ └─┘ └┘ └──┘ └─┘
src └────┘ ┴ ┴ └┘ ┴ ┴ ┴
typ └────┘└┘┴└──┘┴└─┘└┘└┘┴└──┘┴└─┘┴
doc └────┘ ┴ ┴ └┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ └┘ ┴ ┴ ┴
par └────┘ ┴ ┴ └┘ ┴ ┴ ┴
pid ┴┴ ┴ ┴ └┘ ┴ ┴ ┴
st ───┘└─────────────────────────────┘└─
362 symmetry, apply tactic.ring.horner_mul_const; refl },
id └──────────────────────────┘
src └──────┘ └────┘└──────────────────────────┘ └───┘
typ └──────┘ └────┘└──────────────────────────┘ └───┘
doc └──────┘ └────┘ └───┘
txt └──────┘ └────┘ └───┘
par └──────┘ └────┘ └───┘
pid ┴ ┴
st ───────────┘└─────────────────────────────────────────┘└┘└
363 { cases cseval_horner' t _ x₁ n₂ 0 csA₂ ⟨0, rfl⟩ with csh₁ h₁,
id └────────────┘ ┴ └┘ └┘ └──┘ └─┘
src └────┘└────────────┘┴ └─┘ ┴ └─┘ ┴ └─┘└─┘└────────────┘
typ └────┘└────────────┘┴┴└─┘└┘┴└┘└─┘└──┘┴ └─┘└─┘└────────────┘
doc └────┘ ┴ └─┘ ┴ └─┘ ┴ └─┘ └────────────┘
txt └────┘ ┴ └─┘ ┴ └─┘ ┴ └─┘ └────────────┘
par └────┘ ┴ └─┘ ┴ └─┘ ┴ └─┘ └────────────┘
pid ┴ ┴ └─┘ ┴ └─┘ ┴ └─┘ ┴└───────────┘
st ───┘└─────────────────────────────────────────────────────────┘└─
364 cases C, split_ifs,
id ┴
src └────┘ └───────┘
typ └────┘┴ └───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴
st ──────────┘└─────────┘└─
365 { subst b₂,
id └┘
src └────┘
typ └────┘└┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────┘└──────┘└─
366 refine ⟨csh₁, h₁.trans (eq.symm _)⟩,
id └──┘ └──────┘ └─────┘
src └─────┘ └┘└──────┘┴ └─────┘└──┘
typ └─────┘ └──┘└┘└──────┘┴ └─────┘└──┘
doc └─────┘ └┘ ┴ └──┘
txt └─────┘ └┘ ┴ └──┘
par └─────┘ └┘ ┴ └──┘
pid ┴ └┘ ┴ └──┘
st ────────────────────────────────────────┘└─
367 apply tactic.ring.horner_mul_horner_zero; try {refl},
id └────────────────────────────────┘
src └────┘└────────────────────────────────┘ └───┘└──┘┴
typ └────┘└────────────────────────────────┘ └───┘└──┘┴
doc └────┘ └───┘└──┘┴
txt └────┘ └───┘└──┘┴
par └────┘ └───┘└──┘┴
pid ┴ └─────┘
st ────────────────────────────────────────────────────┘└──┘└┘└
368 simp! [hA₂] },
id └─┘
src └─────┘ └┘
typ └─────┘└─┘└┘
doc └─────┘ └┘
txt └─────┘ └┘
par └─────┘ └┘
pid ┴┴┴ ┴┴
st ─────────────────┘└┘└
369 { cases A₁ csa₁ csb₂ with csA₁ hA₁,
id └┘ └──┘ └──┘
src └────┘ ┴ ┴ └────────────┘
typ └────┘└┘┴└──┘┴└──┘└────────────┘
doc └────┘ ┴ ┴ └────────────┘
txt └────┘ ┴ ┴ └────────────┘
par └────┘ ┴ ┴ └────────────┘
pid ┴ ┴ ┴ └────────────┘
st ─────────────────────────────────────┘└─
370 cases cseval_add t csh₁ _ with csh₂ h₂,
id └────────┘ ┴ └──┘
src └────┘└────────┘┴ ┴ └─────────────┘
typ └────┘└────────┘┴┴┴└──┘└─────────────┘
doc └────┘ ┴ ┴ └─────────────┘
txt └────┘ ┴ ┴ └─────────────┘
par └────┘ ┴ ┴ └─────────────┘
pid ┴ ┴ ┴ └┘└───────────┘
st ───────────────────────────────────────────┘└─
371 { refine ⟨csh₂, h₂.trans (eq.symm _)⟩,
id └──┘ └──────┘ └─────┘
src └─────┘ └┘└──────┘┴ └─────┘└──┘
typ └─────┘ └──┘└┘└──────┘┴ └─────┘└──┘
doc └─────┘ └┘ ┴ └──┘
txt └─────┘ └┘ ┴ └──┘
par └─────┘ └┘ ┴ └──┘
pid ┴ └┘ ┴ └──┘
st ───────┘└─────────────────────────────────┘└─
372 apply tactic.ring.horner_mul_horner; try {refl},
id └───────────────────────────┘
src └────┘└───────────────────────────┘ └───┘└──┘┴
typ └────┘└───────────────────────────┘ └───┘└──┘┴
doc └────┘ └───┘└──┘┴
txt └────┘ └───┘└──┘┴
par └────┘ └───┘└──┘┴
pid ┴ └─────┘
st ─────────────────────────────────────────────────┘└──┘└┘└
373 simp! * },
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴┴┴┴
st ───────────────┘└┘└
374 exact ⟨csA₁, (B₁ csb₁ csb₂).1⟩ } },
id └──┘ └┘ └──┘ └──┘
src └────┘ └┘ ┴ ┴ └───┘
typ └────┘ └──┘└┘ └┘┴└──┘┴└──┘└───┘
doc └────┘ └┘ ┴ ┴ └───┘
txt └────┘ └┘ ┴ ┴ └───┘
par └────┘ └┘ ┴ ┴ └───┘
pid ┴ └┘ ┴ ┴ └──┘┴
st ────────────────────────────────────┘└──┘└
375 { simp [A₂ csa₂, B₂ csb₂], rw [mul_comm, eq_comm],
id └┘ └──┘ └┘ └──┘ └──────┘ └─────┘
src └────┘ ┴ └┘ ┴ ┴ └──┘└──────┘└┘└─────┘┴
typ └────┘└┘┴└──┘└┘└┘┴└──┘┴ └──┘└──────┘└┘└─────┘┴
doc └────┘ ┴ └┘ ┴ ┴ └──┘ └┘ ┴
txt └────┘ ┴ └┘ ┴ ┴ └──┘ └┘ ┴
par └────┘ ┴ └┘ ┴ ┴ └──┘ └┘ ┴
pid ┴┴ ┴ └┘ ┴ ┴ └┘ └┘ ┴
st ──────────────────────────┘└────────────┘└───────┘┴└─
376 apply tactic.ring.horner_const_mul,
id └──────────────────────────┘
src └────┘└──────────────────────────┘
typ └────┘└──────────────────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────────────────────┘└─
377 {apply mul_comm}, {refl} },
id └──────┘
src └────┘└──────┘ └──┘
typ └────┘└──────┘ └──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴
st ──────────────────┘└┘└────┘└────
378 end
st ──┘
379
380 theorem cseval_pow {α} [comm_semiring α] (t : tree α)
id └───────────┘ ┴ └──┘ ┴
src └───────────┘ └──┘
typ └───────────┘ ┴ └──┘ ┴
381 {x : horner_expr} (cs : x.is_cs) :
id └─────────┘ ┴└────┘
src └─────────┘ └────┘
typ └─────────┘ ┴└────┘
doc └─────────┘ └────┘
382 ∀ (n : num), (pow x n).is_cs ∧
id ┴ └─┘ └─┘ ┴ ┴ └───┘ ┴
src └─┘ └─┘ └───┘ ┴
typ ┴ └─┘ └─┘ ┴ ┴ └───┘ ┴
doc └─┘ └───┘
383 cseval t (pow x n) = cseval t x ^ (n : ℕ)
id └────┘ ┴ └─┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
src └────┘ └─┘ ┴ └────┘ ┴ ┴
typ └────┘ ┴ └─┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ ┴
doc └────┘ └────┘
384 | 0 := ⟨⟨1, rfl⟩, (pow_zero _).symm⟩
id └─┘ └──────┘ └──┘
src └─┘ └──────┘ └──┘
typ └─┘ └──────┘ └──┘
385 | (num.pos p) := begin
id └─────┘
src └─────┘
typ └─────┘
st └─────
386 simp [pow], induction p with p ep p ep,
id └─┘ ┴
src └────┘└─┘┴ └────────┘ └─────────────┘
typ └────┘└─┘┴ └────────┘┴└─────────────┘
doc └────┘ ┴ └────────┘ └─────────────┘
txt └────┘ ┴ └────────┘ └─────────────┘
par └────┘ ┴ └────────┘ └─────────────┘
pid ┴┴ ┴ ┴ ┴└────────────┘
st ───────────┘└──────────────────────────┘└─
387 { simp * },
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid ┴┴┴
st ───┘└─────┘└┘└
388 { simp [pow_bit1],
id └──────┘
src └────┘└──────┘┴
typ └────┘└──────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ───┘└─────────────┘└─
389 cases cseval_mul t ep.1 ep.1 with cs₀ h₀,
id └────────┘ ┴ └┘
src └────┘└────────┘┴ ┴ └─┘ └────────────┘
typ └────┘└────────┘┴┴┴ └─┘└┘└────────────┘
doc └────┘ ┴ ┴ └─┘ └────────────┘
txt └────┘ ┴ ┴ └─┘ └────────────┘
par └────┘ ┴ ┴ └─┘ └────────────┘
pid ┴ ┴ ┴ └─┘ └────────────┘
st ───────────────────────────────────────────┘└─
390 cases cseval_mul t cs₀ cs with cs₁ h₁,
id └────────┘ ┴ └─┘ └┘
src └────┘└────────┘┴ ┴ ┴ └──────────┘
typ └────┘└────────┘┴┴┴└─┘┴└┘└──────────┘
doc └────┘ ┴ ┴ ┴ └──────────┘
txt └────┘ ┴ ┴ ┴ └──────────┘
par └────┘ ┴ ┴ ┴ └──────────┘
pid ┴ ┴ ┴ ┴ └──────────┘
st ────────────────────────────────────────┘└─
391 simp * },
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid ┴┴┴
st ──────────┘└┘└
392 { simp [pow_bit0],
id └──────┘
src └────┘└──────┘┴
typ └────┘└──────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ──────────────────┘└─
393 cases cseval_mul t ep.1 ep.1 with cs₀ h₀,
id └────────┘ ┴ └┘
src └────┘└────────┘┴ ┴ └─┘ └────────────┘
typ └────┘└────────┘┴┴┴ └─┘└┘└────────────┘
doc └────┘ ┴ ┴ └─┘ └────────────┘
txt └────┘ ┴ ┴ └─┘ └────────────┘
par └────┘ ┴ ┴ └─┘ └────────────┘
pid ┴ ┴ ┴ └─┘ └────────────┘
st ───────────────────────────────────────────┘└─
394 simp * }
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid ┴┴┴
st ──────────┘└─
395 end
st ──┘
396
397 /-- For any given tree `t` of atoms and any reflected expression `r`,
398 the Horner form of `r` is a valid csring expression, and under `t`,
399 the Horner form evaluates to the same thing as `r`. -/
400 theorem cseval_of_csexpr {α} [comm_semiring α] (t : tree α) :
id └───────────┘ ┴ └──┘ ┴
src └───────────┘ └──┘
typ └───────────┘ ┴ └──┘ ┴
401 ∀ (r : csring_expr), (of_csexpr r).is_cs ∧ cseval t (of_csexpr r) = r.eval t
id ┴ └─────────┘ └───────┘ ┴ └───┘ ┴ └────┘ ┴ └───────┘ ┴ ┴ ┴└───┘ ┴
src └─────────┘ └───────┘ └───┘ ┴ └────┘ └───────┘ ┴ └───┘
typ ┴ └─────────┘ └───────┘ ┴ └───┘ ┴ └────┘ ┴ └───────┘ ┴ ┴ ┴└───┘ ┴
doc └─────────┘ └───────┘ └───┘ └────┘ └───────┘ └───┘
402 | (csring_expr.atom n) := cseval_atom _ _
id └──────────────┘ └─────────┘
src └──────────────┘ └─────────┘
typ └──────────────┘ └─────────┘
403 | (csring_expr.const n) := ⟨⟨n, rfl⟩, by cases n; refl⟩
id └───────────────┘ ┴ └─┘ ┴
src └───────────────┘ └─┘ └────┘ └──┘
typ └───────────────┘ ┴ └─┘ └────┘┴ └──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴
st └────────────┘
404 | (csring_expr.add x y) :=
id └─────────────┘ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴
405 let ⟨cs₁, h₁⟩ := cseval_of_csexpr x,
id └─┘ └─┘ └──────────────┘
typ └─┘ └─┘ └──────────────┘
406 ⟨cs₂, h₂⟩ := cseval_of_csexpr y,
id └─┘ └──────────────┘
typ └─┘ └──────────────┘
407 ⟨cs, h⟩ := cseval_add t cs₁ cs₂ in ⟨cs, by simp! [h, *]⟩
id └┘ └────────┘ ┴ ┴
src └────────┘ └─────┘ └──┘
typ └┘ └────────┘ ┴ └─────┘┴└──┘
doc └─────┘ └──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴┴┴ └──┘
st └───────────┘
408 | (csring_expr.mul x y) :=
id └─────────────┘ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴
409 let ⟨cs₁, h₁⟩ := cseval_of_csexpr x,
id └─┘ └─┘ └──────────────┘
typ └─┘ └─┘ └──────────────┘
410 ⟨cs₂, h₂⟩ := cseval_of_csexpr y,
id └─┘ └──────────────┘
typ └─┘ └──────────────┘
411 ⟨cs, h⟩ := cseval_mul t cs₁ cs₂ in ⟨cs, by simp! [h, *]⟩
id └┘ └────────┘ ┴ ┴
src └────────┘ └─────┘ └──┘
typ └┘ └────────┘ ┴ └─────┘┴└──┘
doc └─────┘ └──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴┴┴ └──┘
st └───────────┘
412 | (csring_expr.pow x n) :=
id └─────────────┘ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴
413 let ⟨cs, h⟩ := cseval_of_csexpr x,
id └─┘ └┘ └──────────────┘
typ └─┘ └┘ └──────────────┘
414 ⟨cs, h⟩ := cseval_pow t cs n in ⟨cs, by simp! [h, *]⟩
id └┘ └────────┘ ┴ ┴
src └────────┘ └─────┘ └──┘
typ └┘ └────────┘ ┴ └─────┘┴└──┘
doc └─────┘ └──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴┴┴ └──┘
st └───────────┘
415
416 end horner_expr
417
418 /-- The main proof-by-reflection theorem. Given reflected csring expressions
419 `r₁` and `r₂` plus a storage `t` of atoms, if both expressions go to the
420 same Horner normal form, then the original non-reflected expressions are
421 equal. `H` follows from kernel reduction and is therefore `rfl`. -/
422 theorem correctness {α} [comm_semiring α] (t : tree α) (r₁ r₂ : csring_expr)
id └───────────┘ ┴ └──┘ ┴ └─────────┘
src └───────────┘ └──┘ └─────────┘
typ └───────────┘ ┴ └──┘ ┴ └─────────┘
doc └─────────┘
423 (H : horner_expr.of_csexpr r₁ = horner_expr.of_csexpr r₂) :
id └───────────────────┘ └┘ ┴ └───────────────────┘ └┘
src └───────────────────┘ ┴ └───────────────────┘
typ └───────────────────┘ └┘ ┴ └───────────────────┘ └┘
doc └───────────────────┘ └───────────────────┘
424 r₁.eval t = r₂.eval t :=
id └┘└───┘ ┴ ┴ └┘└───┘ ┴
src └───┘ ┴ └───┘
typ └┘└───┘ ┴ ┴ └┘└───┘ ┴
doc └───┘ └───┘
425 by repeat {rw ← (horner_expr.cseval_of_csexpr t _).2}; rw H
id └──────────────────────────┘ ┴ ┴
src └──────┘└───┘ └──────────────────────────┘┴ └───┘┴ └─┘ └
typ └──────┘└───┘ └──────────────────────────┘┴┴└───┘┴ └─┘┴└
doc └──────┘└───┘ └──────────────────────────┘┴ └───┘┴ └─┘ └
txt └──────┘└───┘ ┴ └───┘┴ └─┘ └
par └──────┘└───┘ ┴ └───┘┴ └─┘ └
pid └─────┘ ┴ └────┘ ┴ └
st └────────────────────────────────────────────────┘└┘└──┘┴└
426
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
427 /-- Reflects a csring expression into a `csring_expr`, together
428 with a dlist of atoms, i.e. opaque variables over which the
429 expression is a polynomial. -/
430 meta def reflect_expr : expr → csring_expr × dlist expr
id └──┘ ┴ └─────────┘ ┴ └───┘ └──┘
src └──┘ └─────────┘ ┴ └───┘ └──┘
typ └──┘ ┴ └─────────┘ ┴ └───┘ └──┘
doc └──┘ └─────────┘ └───┘ └──┘
431 | `(%%e₁ + %%e₂) :=
id └┘ ┴ └┘
src ┴
typ └┘ ┴ └┘
432 let (r₁, l₁) := reflect_expr e₁, (r₂, l₂) := reflect_expr e₂ in
id └─┘ ┴└┘ └┘ └──────────┘ ┴└┘ └┘ └──────────┘
src ┴ ┴
typ └─┘ ┴└┘ └┘ └──────────┘ ┴└┘ └┘ └──────────┘
433 (r₁.add r₂, l₁ ++ l₂)
id ┴ └──┘ └┘
src ┴ └──┘ └┘
typ ┴ └──┘ └┘
434 /-| `(%%e₁ - %%e₂) :=
435 let (r₁, l₁) := reflect_expr e₁, (r₂, l₂) := reflect_expr e₂ in
436 (r₁.add r₂.neg, l₁ ++ l₂)
437 | `(- %%e) := let (r, l) := reflect_expr e in (r.neg, l)-/
438 | `(%%e₁ * %%e₂) :=
id └┘ ┴ └┘
src ┴
typ └┘ ┴ └┘
439 let (r₁, l₁) := reflect_expr e₁, (r₂, l₂) := reflect_expr e₂ in
id └─┘ ┴└┘ └┘ └──────────┘ ┴└┘ └┘ └──────────┘
src ┴ ┴
typ └─┘ ┴└┘ └┘ └──────────┘ ┴└┘ └┘ └──────────┘
440 (r₁.mul r₂, l₁ ++ l₂)
id ┴ └──┘ └┘
src ┴ └──┘ └┘
typ ┴ └──┘ └┘
441 /-| `(has_inv.inv %%e) := let (r, l) := reflect_expr e in (r.neg, l)
442 | `(%%e₁ / %%e₂) :=
443 let (r₁, l₁) := reflect_expr e₁, (r₂, l₂) := reflect_expr e₂ in
444 (r₁.mul r₂.inv, l₁ ++ l₂)-/
445 | e@`(%%e₁ ^ %%e₂) :=
id └┘ ┴ └┘
src ┴
typ └┘ ┴ └┘
446 match reflect_expr e₁, expr.to_nat e₂ with
id └──────────┘ └─────────┘
src └─────────┘
typ └──────────┘ └─────────┘
doc └─────────┘
447 | (r₁, l₁), some n₂ := (r₁.pow (num.of_nat' n₂), l₁)
id ┴└┘ └┘ └──┘ └┘ ┴ └──┘ └─────────┘
src ┴ └──┘ ┴ └──┘ └─────────┘
typ ┴└┘ └┘ └──┘ └┘ ┴ └──┘ └─────────┘
448 | (r₁, l₁), none := (csring_expr.atom 1, dlist.singleton e)
id ┴ └──┘ ┴└──────────────┘ └─────────────┘
src ┴ └──┘ ┴└──────────────┘ └─────────────┘
typ ┴ └──┘ ┴└──────────────┘ └─────────────┘
doc └─────────────┘
449 end
450 | e := match expr.to_nat e with
id ┴ └─────────┘
src └─────────┘
typ ┴ └─────────┘
doc └─────────┘
451 | some n := (csring_expr.const (num.of_nat' n), dlist.empty)
id └──┘ ┴ ┴└───────────────┘ └─────────┘ └─────────┘
src └──┘ ┴└───────────────┘ └─────────┘ └─────────┘
typ └──┘ ┴ ┴└───────────────┘ └─────────┘ └─────────┘
doc └─────────┘
452 | none := (csring_expr.atom 1, dlist.singleton e)
id └──┘ ┴└──────────────┘ └─────────────┘
src └──┘ ┴└──────────────┘ └─────────────┘
typ └──┘ ┴└──────────────┘ └─────────────┘
doc └─────────────┘
453 end
454
455 /-- In the output of `reflect_expr`, `atom`s are initialized with incorrect indices.
456 The indices cannot be computed until the whole tree is built, so another pass over
457 the expressions is needed - this is what `replace` does. The computation (expressed
458 in the state monad) fixes up `atom`s to match their positions in the atom tree.
459 The initial state is a list of all atom occurrences in the goal, left-to-right. -/
460 meta def csring_expr.replace (t : tree expr) : csring_expr → state_t (list expr) option csring_expr
id └──┘ └──┘ └─────────┘ ┴ └─────┘ └──┘ └──┘ └────┘ └─────────┘
src └──┘ └──┘ └─────────┘ └─────┘ └──┘ └──┘ └────┘ └─────────┘
typ └──┘ └──┘ └─────────┘ ┴ └─────┘ └──┘ └──┘ └────┘ └─────────┘
doc └──┘ └─────────┘ └──┘ └─────────┘
461 | (csring_expr.atom _) := do e ← get,
id └──────────────┘ ┴ └─┘
src └──────────────┘ └─┘
typ └──────────────┘ ┴ └─┘
doc └─┘
462 p ← monad_lift (t.index_of (<) e.head),
id ┴ └────────┘ ┴└───────┘ ┴ ┴└───┘
src └────────┘ └───────┘ ┴ └───┘
typ ┴ └────────┘ ┴└───────┘ ┴ ┴└───┘
doc └───────┘
463 put e.tail, pure (csring_expr.atom p)
id └─┘ ┴└───┘ └──┘ └──────────────┘ ┴
src └─┘ └───┘ └──┘ └──────────────┘
typ └─┘ ┴└───┘ └──┘ └──────────────┘ ┴
doc └─┘
464 | (csring_expr.const n) := pure (csring_expr.const n)
id └───────────────┘ ┴ └──┘ └───────────────┘
src └───────────────┘ └──┘ └───────────────┘
typ └───────────────┘ ┴ └──┘ └───────────────┘
465 | (csring_expr.add x y) := csring_expr.add <$> x.replace <*> y.replace
id └─────────────┘ ┴ ┴ └─────────────┘ └─┘ └─┘
src └─────────────┘ └─────────────┘ └─┘ └─┘
typ └─────────────┘ ┴ ┴ └─────────────┘ └─┘ └─┘
466 | (csring_expr.mul x y) := csring_expr.mul <$> x.replace <*> y.replace
id └─────────────┘ ┴ ┴ └─────────────┘ └─┘ └─┘
src └─────────────┘ └─────────────┘ └─┘ └─┘
typ └─────────────┘ ┴ ┴ └─────────────┘ └─┘ └─┘
467 | (csring_expr.pow x n) := (λ x, csring_expr.pow x n) <$> x.replace
id └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ └─┘
src └─────────────┘ └─────────────┘ └─┘
typ └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ └─┘
468 --| (csring_expr.neg x) := csring_expr.neg <$> x.replace
469 --| (csring_expr.inv x) := csring_expr.inv <$> x.replace
470
471 end tactic.ring2
472
473 namespace tactic
474 namespace interactive
475 open interactive interactive.types lean.parser
476 open tactic.ring2
477
478 local postfix `?`:9001 := optional
id └──────┘
src └──────┘
typ └──────┘
479
480 /-- Tactic for solving equations in the language of rings.
481 This variant on the `ring` tactic uses kernel computation instead
482 of proof generation. -/
483 meta def ring2 : tactic unit :=
id └────┘ └──┘
src └────┘ └──┘
typ └────┘ └──┘
doc └──┘
484 do `[repeat {rw ← nat.pow_eq_pow}],
src └──────┘└───┘ ┴
typ └──────┘└───┘ ┴
doc └──────┘└───┘ ┴
txt └──────┘└───┘ ┴
par └──────┘└───┘ ┴
pid └─────┘ ┴
485 `(%%e₁ = %%e₂) ← target
id └┘ └┘ ┴ └┘ └────┘
src └┘ ┴ └────┘
typ └┘ └┘ ┴ └┘ └────┘
doc └┘ └────┘
486 | fail "ring2 tactic failed: the goal is not an equality",
id └──┘
src └──┘
typ └──┘
487 α ← infer_type e₁,
id ┴ └────────┘
src └────────┘
typ ┴ └────────┘
doc └────────┘
488 expr.sort (level.succ u) ← infer_type α,
id └───────┘ └────────┘ ┴ └────────┘ ┴
src └───────┘ └────────┘ └────────┘
typ └───────┘ └────────┘ ┴ └────────┘ ┴
doc └────────┘
489 let (r₁, l₁) := reflect_expr e₁,
id └─┘ ┴└┘ └┘ └──────────┘
src ┴ └──────────┘
typ └─┘ ┴└┘ └┘ └──────────┘
doc └──────────┘
490 let (r₂, l₂) := reflect_expr e₂,
id ┴└┘ └┘ └──────────┘
src ┴ └──────────┘
typ ┴└┘ └┘ └──────────┘
doc └──────────┘
491 let L := (l₁ ++ l₂).to_list,
id ┴ └┘ └─────┘
src └┘ └─────┘
typ ┴ └┘ └─────┘
doc └─────┘
492 let s := tree.of_rbnode (rbtree_of L).1,
id ┴ └────────────┘ └───────┘ ┴ ┴
src └────────────┘ └───────┘ ┴
typ ┴ └────────────┘ └───────┘ ┴ ┴
doc └────────────┘
493 (r₁, L) ← (state_t.run (r₁.replace s) L : option _),
id ┴└┘ ┴ └─────────┘ └──────┘ ┴ ┴ └────┘
src ┴ └─────────┘ └──────┘ └────┘
typ ┴└┘ ┴ └─────────┘ └──────┘ ┴ ┴ └────┘
doc └──────┘
494 (r₂, _) ← (state_t.run (r₂.replace s) L : option _),
id ┴└┘ └─────────┘ └──────┘ ┴ └────┘
src ┴ └─────────┘ └──────┘ └────┘
typ ┴└┘ └─────────┘ └──────┘ ┴ └────┘
doc └──────┘
495 let se : expr := s.reflect' u α,
id └──┘ ┴└───────┘ ┴
src └──┘ └───────┘
typ └──┘ ┴└───────┘ ┴
doc └──┘ └───────┘
496 let er₁ : expr := reflect r₁,
id └──┘ └─────┘
src └──┘ └─────┘
typ └──┘ └─────┘
doc └──┘
497 let er₂ : expr := reflect r₂,
id └──┘ └─────┘
src └──┘ └─────┘
typ └──┘ └─────┘
doc └──┘
498 cs ← mk_app ``comm_semiring [α] >>= mk_instance,
id └┘ └────┘ ┴ ┴┴┴ └─┘ └─────────┘
src └────┘ ┴ ┴ ┴ └─┘ └─────────┘
typ └┘ └────┘ ┴ ┴┴┴ └─┘ └─────────┘
doc └────┘ └─────────┘
499 e ← to_expr ``(correctness %%se %%er₁ %%er₂ rfl)
id ┴ └─────┘ └─────────┘ └┘ └─┘ └─┘ └─┘
src └─────┘ └─────────┘ └─┘
typ ┴ └─────┘ └─────────┘ └┘ └─┘ └─┘ └─┘
doc └─────┘ └─────────┘
500 <|> fail ("ring2 tactic failed, cannot show equality:\n"
id └─┘ └──┘
src └─┘ └──┘
typ └─┘ └──┘
501 ++ to_string (horner_expr.of_csexpr r₁) ++
id └┘ └───────┘ └───────────────────┘ └┘
src └┘ └───────┘ └───────────────────┘ └┘
typ └┘ └───────┘ └───────────────────┘ └┘
doc └───────────────────┘
502 "\n =?=\n" ++ to_string (horner_expr.of_csexpr r₂)),
id └┘ └───────┘ └───────────────────┘
src └┘ └───────┘ └───────────────────┘
typ └┘ └───────┘ └───────────────────┘
doc └───────────────────┘
503 tactic.exact e
id └──────────┘ ┴
src └──────────┘
typ └──────────┘ ┴
doc └──────────┘
504
505 end interactive
506 end tactic
507
508 namespace conv.interactive
509 open conv
510
511 meta def ring2 : conv unit := discharge_eq_lhs tactic.interactive.ring2
id └──┘ └──┘ └──────────────┘ └──────────────────────┘
src └──┘ └──┘ └──────────────┘ └──────────────────────┘
typ └──┘ └──┘ └──────────────┘ └──────────────────────┘
doc └──┘ └──────────────────────┘
512
513 end conv.interactive